diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/datatype_realizer.ML
--- 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;