--- 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])