--- a/src/HOL/Tools/datatype_realizer.ML Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Oct 15 22:00:28 2021 +0200
@@ -112,14 +112,14 @@
val thm =
Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
- (fn {context = goal_ctxt, prems} =>
+ (fn prems =>
EVERY [
- rewrite_goals_tac goal_ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
- resolve_tac goal_ctxt [infer_instantiate goal_ctxt inst induct] 1,
- ALLGOALS (Object_Logic.atomize_prems_tac goal_ctxt),
- rewrite_goals_tac goal_ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
- REPEAT ((resolve_tac goal_ctxt prems THEN_ALL_NEW (fn i =>
- REPEAT (eresolve_tac goal_ctxt [allE] i) THEN assume_tac goal_ctxt i)) 1)])
+ rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
+ resolve_tac ctxt [infer_instantiate ctxt inst induct] 1,
+ ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
+ rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
+ REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i =>
+ REPEAT (eresolve_tac ctxt [allE] i) THEN assume_tac ctxt i)) 1)])
|> Drule.export_without_context;
val ind_name = Thm.derivation_name induct;
@@ -190,13 +190,12 @@
Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems)
(Thm.cterm_of ctxt
(HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
- (fn {context = goal_ctxt, prems} =>
- EVERY [
- resolve_tac goal_ctxt
- [infer_instantiate goal_ctxt [(#1 (dest_Var y), Thm.cterm_of goal_ctxt y')] exhaust] 1,
+ (fn prems =>
+ EVERY [
+ resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1,
ALLGOALS (EVERY'
- [asm_simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps case_rewrites),
- resolve_tac goal_ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss goal_ctxt)])])
+ [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
+ resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
|> Drule.export_without_context;
val exh_name = Thm.derivation_name exhaust;