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