diff -r a1aa42743d7d -r 823ccd84b879 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Oct 15 21:59:46 2021 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Oct 15 22:00:28 2021 +0200
@@ -260,9 +260,8 @@
       |> HOLogic.mk_Trueprop
       |> Logic.all x_uc;
 
-    val mono_thm =
-      Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
-        (fn {context = goal_ctxt, ...} => mono_tac goal_ctxt 1)
+    val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
+        (K (mono_tac lthy 1))
     val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm
 
     val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);