src/HOL/Tools/Function/partial_function.ML

              SOME (nth args (arity - 1), conv)
            end)
   | _ => 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
          NONE => no_tac
        | SOME (arg, conv) =>
            let open Conv in
               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
            end)
   | _ => no_tac) 1);
 
 (*monotonicity proof: apply rules + split case expressions*)
 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));
 
 
 (*** Auxiliary functions ***)
 

 
     val raw_induct = Option.map mk_raw_induct fixp_induct_user
     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])
     |-> (fn (_, rec') =>
       Spec_Rules.add Spec_Rules.Equational ([f], rec')