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] ;