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