diff -r c960bfcb91db -r bbfed17243af src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Oct 15 19:25:31 2021 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Oct 15 20:54:13 2021 +0200
@@ -260,8 +260,9 @@
       |> HOLogic.mk_Trueprop
       |> Logic.all x_uc;
 
-    val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
-        (K (mono_tac lthy 1))
+    val mono_thm =
+      Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
+        (fn {context = goal_ctxt, ...} => mono_tac goal_ctxt 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);