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