diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -80,7 +80,7 @@
   | _ => NONE;
 
 (*split on case expressions*)
-val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context=ctxt, ...} =>
+val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} =>
   SUBGOAL (fn (t, i) => case t of
     _ $ (_ $ Abs (_, _, body)) =>
       (case dest_case ctxt body of
@@ -90,7 +90,7 @@
               if Term.is_open arg then no_tac
               else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
                 THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
-                THEN_ALL_NEW eresolve_tac @{thms thin_rl}
+                THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
                 THEN_ALL_NEW (CONVERSION
                   (params_conv ~1 (fn ctxt' =>
                     arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
@@ -101,7 +101,7 @@
 fun mono_tac ctxt =
   K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
   THEN' (TRY o REPEAT_ALL_NEW
-   (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems partial_function_mono}))
+   (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems partial_function_mono}))
      ORELSE' split_cases_tac ctxt));
 
 
@@ -290,7 +290,7 @@
     val rec_rule = let open Conv in
       Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
         CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
-        THEN resolve_tac @{thms refl} 1) end;
+        THEN resolve_tac lthy' @{thms refl} 1) end;
   in
     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])