diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Fri Oct 15 19:25:31 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Fri Oct 15 20:54:13 2021 +0200
@@ -708,12 +708,12 @@
   in
     Goal.prove_internal ctxt' []
       (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\<open>bool\<close>))))
-      (fn _ =>
-        resolve_tac ctxt' [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN
-        (resolve_tac ctxt' [rule]
+      (fn {context = goal_ctxt, ...} =>
+        resolve_tac goal_ctxt [thm2 RS @{thm transfer_start'}, thm2 RS @{thm transfer_start}] 1 THEN
+        (resolve_tac goal_ctxt [rule]
           THEN_ALL_NEW
-            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
-              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
+            (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules)
+              THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1
           handle TERM (_, ts) =>
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps
@@ -744,12 +744,12 @@
   in
     Goal.prove_internal ctxt' []
       (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), \<^typ>\<open>bool\<close>))))
-      (fn _ =>
-        resolve_tac ctxt' [thm2 RS @{thm untransfer_start}] 1 THEN
-        (resolve_tac ctxt' [rule]
+      (fn {context = goal_ctxt, ...} =>
+        resolve_tac goal_ctxt [thm2 RS @{thm untransfer_start}] 1 THEN
+        (resolve_tac goal_ctxt [rule]
           THEN_ALL_NEW
-            (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
-              THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
+            (SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt rules)
+              THEN_ALL_NEW (DETERM o eq_rules_tac goal_ctxt eq_rules)))) 1
           handle TERM (_, ts) =>
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps