diff -r 0c5cd369a643 -r 50b60f501b05 src/Pure/Isar/proof.ML
--- 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