--- a/src/Pure/Isar/proof.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Pure/Isar/proof.ML Tue Feb 10 14:48:26 2015 +0100
@@ -440,12 +440,12 @@
Goal.norm_hhf_tac ctxt THEN'
SUBGOAL (fn (goal, i) =>
if can Logic.unprotect (Logic.strip_assums_concl goal) then
- eresolve_tac [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
+ eresolve_tac ctxt [Drule.protectI] i THEN finish_tac ctxt (n - 1) i
else finish_tac ctxt (n - 1) (i + 1));
fun goal_tac ctxt rule =
Goal.norm_hhf_tac ctxt THEN'
- resolve_tac [rule] THEN'
+ resolve_tac ctxt [rule] THEN'
finish_tac ctxt (Thm.nprems_of rule);
fun FINDGOAL tac st =
@@ -883,9 +883,9 @@
in map (Logic.mk_term o Var) vars end;
fun refine_terms n =
- refine (Method.Basic (K (NO_CASES o
+ refine (Method.Basic (fn ctxt => NO_CASES o
K (HEADGOAL (PRECISE_CONJUNCTS n
- (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac [Drule.termI])))))))))
+ (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))))
#> Seq.hd;
in