src/FOLP/intprover.ML
changeset 9263 53e09e592278
parent 4440 9ed4098074bc
child 15570 8d8c70b41bab
--- a/src/FOLP/intprover.ML	Thu Jul 06 12:27:37 2000 +0200
+++ b/src/FOLP/intprover.ML	Thu Jul 06 13:11:32 2000 +0200
@@ -54,7 +54,7 @@
 
 (*Attack subgoals using safe inferences*)
 val safe_step_tac = FIRST' [uniq_assume_tac,
-                            IFOLP_Lemmas.uniq_mp_tac,
+                            int_uniq_mp_tac,
                             biresolve_tac safe0_brls,
                             hyp_subst_tac,
                             biresolve_tac safep_brls] ;