Fix a few proof failures due to changes in HOL

CakeML · May 18, 2020 · e4c7de8 · e4c7de8
1 parent 5ada842
commit e4c7de8
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/candle/overloading/syntax/holSyntaxCyclicityScript.sml b/candle/overloading/syntax/holSyntaxCyclicityScript.sml
@@ -1419,6 +1419,9 @@ Proof
   >> imp_res_tac MEM_TAKE
   >> qspecl_then [`rs'`,`TAKE (LENGTH rs') rs`,`TAKE (LENGTH rs') pqs`,`ctxt`,`es`] assume_tac sol_mon_prop
   >> rfs[sol_seq_TAKE,EVERY_MEM,MEM_TAKE,ELIM_UNCURRY]
+  >> pop_assum mp_tac
+  >> impl_tac >- (rw [] >> imp_res_tac MEM_TAKE >> res_tac)
+  >> strip_tac
   >> first_x_assum (qspec_then `PRE (LENGTH rs')` assume_tac)
   >> first_x_assum (qspec_then `PRE (LENGTH rs')` assume_tac)
   >> `PRE (LENGTH rs') < LENGTH rs'` by fs[prim_recTheory.LESS_SUC_REFL]
@@ -3211,7 +3214,8 @@ Proof
     >- (
       qpat_x_assum `!i. _ ==> ?rs. _` (qspec_then `i` mp_tac)
       >> `i <= LENGTH pqs` by fs[]
-      >> drule_then drule EVERY_TAKE
+      >> drule EVERY_TAKE
+      >> disch_then (qspec_then ‘i’ assume_tac)
       >> rw[is_instance_LR_eq,TAKE_LENGTH_ID]
       >> drule mg_sol_ext1
       >> qmatch_asmsub_abbrev_tac `LR_TYPE_SUBST s (FST pq) = _`
@@ -3267,7 +3271,6 @@ Proof
   >- fs[mg_sol_seq_def,sol_seq_def]
   >- (
     drule EVERY_TAKE
-    >> disch_then match_mp_tac
     >> fs[]
   )
   >- (