src/FOL/intprover.ML
changeset 58957 c9e744ea8a38
parent 51798 ad3a241def73
child 58963 26bf09b95dda
     1.1 --- a/src/FOL/intprover.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/FOL/intprover.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -66,9 +66,9 @@
     1.4    FIRST' [
     1.5      eq_assume_tac,
     1.6      eq_mp_tac,
     1.7 -    bimatch_tac safe0_brls,
     1.8 +    bimatch_tac ctxt safe0_brls,
     1.9      hyp_subst_tac ctxt,
    1.10 -    bimatch_tac safep_brls];
    1.11 +    bimatch_tac ctxt safep_brls];
    1.12  
    1.13  (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
    1.14  fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);