changeset 60754 | 02924903a6fd |
parent 59498 | 50b60f501b05 |
--- a/src/FOLP/intprover.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/FOLP/intprover.ML Sat Jul 18 20:54:56 2015 +0200 @@ -55,7 +55,7 @@ fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, int_uniq_mp_tac ctxt, biresolve_tac ctxt safe0_brls, - hyp_subst_tac, + hyp_subst_tac ctxt, biresolve_tac ctxt safep_brls] ; (*Repeatedly attack subgoals using safe inferences*)