--- 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);