Fix another MEM_DROP issue in holSyntaxExtra

CakeML · Jul 2, 2019 · d697572 · d697572
1 parent 599312a
commit d697572
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/candle/standard/syntax/holSyntaxExtraScript.sml b/candle/standard/syntax/holSyntaxExtraScript.sml
@@ -2585,7 +2585,7 @@ Proof
         metis_tac[] ) >>
       conj_tac >- metis_tac[ALL_DISTINCT_DROP] >>
       rw[] >> spose_not_then strip_assume_tac >>
-      imp_res_tac rich_listTheory.MEM_DROP >>
+      imp_res_tac rich_listTheory.MEM_DROP_IMP >>
       metis_tac[]) >>
     metis_tac[]) >>
   rw[UNCURRY] >>