# HG changeset patch
# User wenzelm
# Date 1684871016 -7200
# Node ID 4d9349989d949ad752ef19cff183d0df2e7da053
# Parent  2cd7e5518d0d68d06a956cc5e8fe5f20cfeefb32
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;

diff -r 2cd7e5518d0d -r 4d9349989d94 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Tue May 23 21:43:36 2023 +0200
@@ -840,9 +840,9 @@
 
 (*<*)experiment begin(*>*)
 simproc_setup unit ("x::unit") =
-  \<open>fn _ => fn _ => fn ct =>
+  \<open>K (K (fn ct =>
     if HOLogic.is_unit (Thm.term_of ct) then NONE
-    else SOME (mk_meta_eq @{thm unit_eq})\<close>
+    else SOME (mk_meta_eq @{thm unit_eq})))\<close>
 (*<*)end(*>*)
 
 text \<open>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Bali/Eval.thy	Tue May 23 21:43:36 2023 +0200
@@ -851,28 +851,28 @@
   by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
 
 simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))))\<close>
 
 simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm eval_var_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm eval_var_eq}))))\<close>
 
 simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))))\<close>
 
 simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))))\<close>
 
 ML \<open>
 ML_Thms.bind_thms ("AbruptIs", sum3_instantiate \<^context> @{thm eval.Abrupt})
@@ -947,10 +947,10 @@
 done
 
 simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>None\<close>, _)) $ _) $ _  $ _ $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
+    | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))))
 \<close>
 
 
@@ -967,10 +967,10 @@
 done
 
 simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>Some\<close>, _) $ _)$ _)) => NONE
-    | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
+    | _ => SOME (mk_meta_eq @{thm eval_abrupt}))))
 \<close>
 
 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<rightarrow> s"
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Bali/Evaln.thy	Tue May 23 21:43:36 2023 +0200
@@ -269,28 +269,28 @@
   by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
 
 simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))))\<close>
 
 simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))))\<close>
 
 simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))))\<close>
 
 simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
-    | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))))\<close>
 
 ML \<open>ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate \<^context> @{thm evaln.Abrupt})\<close>
 declare evaln_AbruptIs [intro!]
@@ -356,11 +356,11 @@
 done
 
 simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ _ $ _ $ (Const (\<^const_name>\<open>Pair\<close>, _) $ (Const (\<^const_name>\<open>Some\<close>,_) $ _)$ _))
         => NONE
-    | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
+    | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))))
 \<close>
 
 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Bali/WellType.thy	Tue May 23 21:43:36 2023 +0200
@@ -605,28 +605,28 @@
   by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
 
 simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
-    | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))))\<close>
 
 simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
-    | _ => SOME (mk_meta_eq @{thm wt_var_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm wt_var_eq}))))\<close>
 
 simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
-    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))))\<close>
 
 simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
-    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))\<close>
+    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))))\<close>
 
 lemma wt_elim_BinOp:
   "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Boolean_Algebras.thy
--- a/src/HOL/Boolean_Algebras.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Boolean_Algebras.thy	Tue May 23 21:43:36 2023 +0200
@@ -513,10 +513,10 @@
 ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
 
 simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
-  \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
+  \<open>K (K (try Boolean_Algebra_Cancel.cancel_sup_conv))\<close>
 
 simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
-  \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
+  \<open>K (K (try Boolean_Algebra_Cancel.cancel_inf_conv))\<close>
 
 
 context boolean_algebra
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Data_Structures/Less_False.thy
--- a/src/HOL/Data_Structures/Less_False.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Data_Structures/Less_False.thy	Tue May 23 21:43:36 2023 +0200
@@ -6,7 +6,7 @@
 imports Main
 begin
 
-simproc_setup less_False ("(x::'a::order) < y") = \<open>fn _ => fn ctxt => fn ct =>
+simproc_setup less_False ("(x::'a::order) < y") = \<open>K (fn ctxt => fn ct =>
   let
     fun prp t thm = Thm.full_prop_of thm aconv t;
 
@@ -25,7 +25,7 @@
              end
          | SOME thm => NONE
       end;
-  in prove_less_False (Thm.term_of ct) end
+  in prove_less_False (Thm.term_of ct) end)
 \<close>
 
 end
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Enum.thy	Tue May 23 21:43:36 2023 +0200
@@ -564,10 +564,10 @@
 by(cases x) simp
 
 simproc_setup finite_1_eq ("x::finite_1") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     (case Thm.term_of ct of
       Const (\<^const_name>\<open>a\<^sub>1\<close>, _) => NONE
-    | _ => SOME (mk_meta_eq @{thm finite_1_eq}))
+    | _ => SOME (mk_meta_eq @{thm finite_1_eq}))))
 \<close>
 
 instantiation finite_1 :: complete_boolean_algebra
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Finite_Set.thy	Tue May 23 21:43:36 2023 +0200
@@ -193,7 +193,7 @@
 lemma finite_subset: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
   by (rule rev_finite_subset)
 
-simproc_setup finite ("finite A") = \<open>fn _ =>
+simproc_setup finite ("finite A") = \<open>
 let
   val finite_subset = @{thm finite_subset}
   val Eq_TrueI = @{thm Eq_TrueI}
@@ -209,17 +209,17 @@
 
   fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths
 
-  fun proc ss ct =
+  fun proc ctxt ct =
     (let
        val _ $ A = Thm.term_of ct
-       val prems = Simplifier.prems_of ss
+       val prems = Simplifier.prems_of ctxt
        val fins = map_filter is_finite prems
        val subsets = map_filter (is_subset A) prems
      in case fold_product comb subsets fins [] of
           (sub_th,fin_th) :: _ => SOME((fin_th RS (sub_th RS finite_subset)) RS Eq_TrueI)
         | _ => NONE
      end)
-in proc end
+in K proc end
 \<close>
 
 (* Needs to be used with care *)
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Fun.thy	Tue May 23 21:43:36 2023 +0200
@@ -1353,7 +1353,7 @@
 
 text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>
 
-simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
+simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>
   let
     fun gen_fun_upd NONE T _ _ = NONE
       | gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y)
@@ -1380,7 +1380,7 @@
                 resolve_tac ctxt @{thms ext} 1 THEN
                 simp_tac (put_simpset ss ctxt) 1)))
       end
-  in proc end
+  in K proc end
 \<close>
 
 
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Groups.thy	Tue May 23 21:43:36 2023 +0200
@@ -178,8 +178,8 @@
       | _ => false)
 \<close>
 
-simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
-simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
+simproc_setup reorient_zero ("0 = x") = \<open>K Reorient_Proc.proc\<close>
+simproc_setup reorient_one ("1 = x") = \<open>K Reorient_Proc.proc\<close>
 
 typed_print_translation \<open>
   let
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/HOL.thy	Tue May 23 21:43:36 2023 +0200
@@ -1236,7 +1236,7 @@
 
 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
 
-simproc_setup neq ("x = y") = \<open>fn _ =>
+simproc_setup neq ("x = y") = \<open>
   let
     val neq_to_EQ_False = @{thm not_sym} RS @{thm Eq_FalseI};
     fun is_neq eq lhs rhs thm =
@@ -1252,7 +1252,7 @@
             SOME thm => SOME (thm RS neq_to_EQ_False)
           | NONE => NONE)
        | _ => NONE);
-  in proc end
+  in K proc end
 \<close>
 
 simproc_setup let_simp ("Let x f") = \<open>
@@ -1266,7 +1266,7 @@
         Abs (_, _, t') => count_loose t' 0 <= 1
       | _ => true);
   in
-    fn _ => fn ctxt => fn ct =>
+    K (fn ctxt => fn ct =>
       if is_trivial_let (Thm.term_of ct)
       then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
       else
@@ -1308,7 +1308,7 @@
                     in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
                 end
             | _ => NONE)
-        end
+        end)
   end
 \<close>
 
@@ -1649,7 +1649,7 @@
 signature REORIENT_PROC =
 sig
   val add : (term -> bool) -> theory -> theory
-  val proc : morphism -> Proof.context -> cterm -> thm option
+  val proc : Proof.context -> cterm -> thm option
 end;
 
 structure Reorient_Proc : REORIENT_PROC =
@@ -1664,7 +1664,7 @@
   fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
 
   val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
-  fun proc phi ctxt ct =
+  fun proc ctxt ct =
     let
       val thy = Proof_Context.theory_of ctxt;
     in
@@ -1851,12 +1851,12 @@
 
 declare [[coercion_args NO_MATCH - -]]
 
-simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>fn _ => fn ctxt => fn ct =>
+simproc_setup NO_MATCH ("NO_MATCH pat val") = \<open>K (fn ctxt => fn ct =>
   let
     val thy = Proof_Context.theory_of ctxt
     val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
     val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
-  in if m then NONE else SOME @{thm NO_MATCH_def} end
+  in if m then NONE else SOME @{thm NO_MATCH_def} end)
 \<close>
 
 text \<open>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Tue May 23 21:43:36 2023 +0200
@@ -142,14 +142,14 @@
 \<close>
 
 simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open>
-  fn phi => fn ctxt => fn ct =>
+  K (fn ctxt => fn ct =>
     let
       val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct)));
       val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
       val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2});
       val rules = Named_Theorems.get ctxt \<^named_theorems>\<open>cont2cont\<close>;
       val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
-    in SOME (perhaps (SINGLE (tac 1)) tr) end
+    in SOME (perhaps (SINGLE (tac 1)) tr) end)
 \<close>
 
 text \<open>Eta-equality for continuous functions\<close>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy	Tue May 23 21:43:36 2023 +0200
@@ -157,7 +157,7 @@
 
 text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
 setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
-simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
+simproc_setup reorient_bottom ("\<bottom> = x") = \<open>K Reorient_Proc.proc\<close>
 
 text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close>
 
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Tue May 23 21:43:36 2023 +0200
@@ -588,15 +588,15 @@
 
 simproc_setup enat_eq_cancel
   ("(l::enat) + m = n" | "(l::enat) = m + n") =
-  \<open>fn phi => fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => Eq_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
 
 simproc_setup enat_le_cancel
   ("(l::enat) + m \<le> n" | "(l::enat) \<le> m + n") =
-  \<open>fn phi => fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => Le_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
 
 simproc_setup enat_less_cancel
   ("(l::enat) + m < n" | "(l::enat) < m + n") =
-  \<open>fn phi => fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => Less_Enat_Cancel.proc ctxt (Thm.term_of ct))\<close>
 
 text \<open>TODO: add regression tests for these simprocs\<close>
 
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 23 21:43:36 2023 +0200
@@ -433,15 +433,15 @@
 
 simproc_setup ennreal_eq_cancel
   ("(l::ennreal) + m = n" | "(l::ennreal) = m + n") =
-  \<open>fn phi => fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => Eq_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
 
 simproc_setup ennreal_le_cancel
   ("(l::ennreal) + m \<le> n" | "(l::ennreal) \<le> m + n") =
-  \<open>fn phi => fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => Le_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
 
 simproc_setup ennreal_less_cancel
   ("(l::ennreal) + m < n" | "(l::ennreal) < m + n") =
-  \<open>fn phi => fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => Less_Ennreal_Cancel.proc ctxt (Thm.term_of ct))\<close>
 
 
 subsection \<open>Order with top\<close>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue May 23 21:43:36 2023 +0200
@@ -1003,28 +1003,28 @@
    "add_mset a m = n" | "m = add_mset a n" |
    "replicate_mset p a = n" | "m = replicate_mset p a" |
    "repeat_mset p m = n" | "m = repeat_mset p m") =
-  \<open>fn phi => Cancel_Simprocs.eq_cancel\<close>
+  \<open>K Cancel_Simprocs.eq_cancel\<close>
 
 simproc_setup msetsubset_cancel
   ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
    "add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
    "replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
    "repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
-  \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
+  \<open>K Multiset_Simprocs.subset_cancel_msets\<close>
 
 simproc_setup msetsubset_eq_cancel
   ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
    "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
    "replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
    "repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
-  \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
+  \<open>K Multiset_Simprocs.subseteq_cancel_msets\<close>
 
 simproc_setup msetdiff_cancel
   ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
    "add_mset a m - n" | "m - add_mset a n" |
    "replicate_mset p r - n" | "m - replicate_mset p r" |
    "repeat_mset p m - n" | "m - repeat_mset p m") =
-  \<open>fn phi => Cancel_Simprocs.diff_cancel\<close>
+  \<open>K Cancel_Simprocs.diff_cancel\<close>
 
 
 subsubsection \<open>Conditionally complete lattice\<close>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Tue May 23 21:43:36 2023 +0200
@@ -776,14 +776,14 @@
    "add_mset a m < n" | "m < add_mset a n" |
    "replicate_mset p a < n" | "m < replicate_mset p a" |
    "repeat_mset p m < n" | "m < repeat_mset p n") =
-  \<open>fn phi => Cancel_Simprocs.less_cancel\<close>
+  \<open>K Cancel_Simprocs.less_cancel\<close>
 
 simproc_setup msetle_cancel
   ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
    "add_mset a m \<le> n" | "m \<le> add_mset a n" |
    "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
    "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
-  \<open>fn phi => Cancel_Simprocs.less_eq_cancel\<close>
+  \<open>K Cancel_Simprocs.less_eq_cancel\<close>
 
 
 subsection \<open>Additional facts and instantiations\<close>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/List.thy	Tue May 23 21:43:36 2023 +0200
@@ -1045,7 +1045,7 @@
         else if lastl aconv lastr then rearr @{thm append_same_eq}
         else NONE
       end;
-  in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end
+  in K (fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct)) end
 \<close>
 
 
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Nat.thy	Tue May 23 21:43:36 2023 +0200
@@ -1968,19 +1968,19 @@
 
 simproc_setup nateq_cancel_sums
   ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_eq_conv)\<close>
 
 simproc_setup natless_cancel_sums
   ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_less_conv)\<close>
 
 simproc_setup natle_cancel_sums
   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_le_conv)\<close>
 
 simproc_setup natdiff_cancel_sums
   ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_diff_conv)\<close>
 
 context order
 begin
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Nonstandard_Analysis/NSA.thy
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Tue May 23 21:43:36 2023 +0200
@@ -549,12 +549,12 @@
   ("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") =
 \<open>
   let val rule = @{thm approx_reorient} RS eq_reflection
-      fun proc phi ss ct =
+      fun proc ct =
         case Thm.term_of ct of
           _ $ t $ u => if can HOLogic.dest_number u then NONE
             else if can HOLogic.dest_number t then SOME rule else NONE
         | _ => NONE
-  in proc end
+  in K (K proc) end
 \<close>
 
 lemma Infinitesimal_approx_minus: "x - y \<in> Infinitesimal \<longleftrightarrow> x \<approx> y"
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Num.thy	Tue May 23 21:43:36 2023 +0200
@@ -1394,7 +1394,7 @@
 \<close>
 
 simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") =
-  Reorient_Proc.proc
+  \<open>K Reorient_Proc.proc\<close>
 
 
 subsubsection \<open>Simplification of arithmetic operations on integer constants\<close>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Tue May 23 21:43:36 2023 +0200
@@ -104,17 +104,17 @@
 
 simproc_setup semiring_assoc_fold
   ("(a::'a::comm_semiring_1_cancel) * b") =
-  \<open>fn phi => Numeral_Simprocs.assoc_fold\<close>
+  \<open>K Numeral_Simprocs.assoc_fold\<close>
 
 (* TODO: see whether the type class can be generalized further *)
 simproc_setup int_combine_numerals
   ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
-  \<open>fn phi => Numeral_Simprocs.combine_numerals\<close>
+  \<open>K Numeral_Simprocs.combine_numerals\<close>
 
 simproc_setup field_combine_numerals
   ("(i::'a::{field,ring_char_0}) + j"
   |"(i::'a::{field,ring_char_0}) - j") =
-  \<open>fn phi => Numeral_Simprocs.field_combine_numerals\<close>
+  \<open>K Numeral_Simprocs.field_combine_numerals\<close>
 
 simproc_setup inteq_cancel_numerals
   ("(l::'a::comm_ring_1) + m = n"
@@ -125,7 +125,7 @@
   |"(l::'a::comm_ring_1) = m * n"
   |"- (l::'a::comm_ring_1) = m"
   |"(l::'a::comm_ring_1) = - m") =
-  \<open>fn phi => Numeral_Simprocs.eq_cancel_numerals\<close>
+  \<open>K Numeral_Simprocs.eq_cancel_numerals\<close>
 
 simproc_setup intless_cancel_numerals
   ("(l::'a::linordered_idom) + m < n"
@@ -136,7 +136,7 @@
   |"(l::'a::linordered_idom) < m * n"
   |"- (l::'a::linordered_idom) < m"
   |"(l::'a::linordered_idom) < - m") =
-  \<open>fn phi => Numeral_Simprocs.less_cancel_numerals\<close>
+  \<open>K Numeral_Simprocs.less_cancel_numerals\<close>
 
 simproc_setup intle_cancel_numerals
   ("(l::'a::linordered_idom) + m \<le> n"
@@ -147,138 +147,138 @@
   |"(l::'a::linordered_idom) \<le> m * n"
   |"- (l::'a::linordered_idom) \<le> m"
   |"(l::'a::linordered_idom) \<le> - m") =
-  \<open>fn phi => Numeral_Simprocs.le_cancel_numerals\<close>
+  \<open>K Numeral_Simprocs.le_cancel_numerals\<close>
 
 simproc_setup ring_eq_cancel_numeral_factor
   ("(l::'a::{idom,ring_char_0}) * m = n"
   |"(l::'a::{idom,ring_char_0}) = m * n") =
-  \<open>fn phi => Numeral_Simprocs.eq_cancel_numeral_factor\<close>
+  \<open>K Numeral_Simprocs.eq_cancel_numeral_factor\<close>
 
 simproc_setup ring_less_cancel_numeral_factor
   ("(l::'a::linordered_idom) * m < n"
   |"(l::'a::linordered_idom) < m * n") =
-  \<open>fn phi => Numeral_Simprocs.less_cancel_numeral_factor\<close>
+  \<open>K Numeral_Simprocs.less_cancel_numeral_factor\<close>
 
 simproc_setup ring_le_cancel_numeral_factor
   ("(l::'a::linordered_idom) * m <= n"
   |"(l::'a::linordered_idom) <= m * n") =
-  \<open>fn phi => Numeral_Simprocs.le_cancel_numeral_factor\<close>
+  \<open>K Numeral_Simprocs.le_cancel_numeral_factor\<close>
 
 (* TODO: remove comm_ring_1 constraint if possible *)
 simproc_setup int_div_cancel_numeral_factors
   ("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
   |"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
-  \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
+  \<open>K Numeral_Simprocs.div_cancel_numeral_factor\<close>
 
 simproc_setup divide_cancel_numeral_factor
   ("((l::'a::{field,ring_char_0}) * m) / n"
   |"(l::'a::{field,ring_char_0}) / (m * n)"
   |"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") =
-  \<open>fn phi => Numeral_Simprocs.divide_cancel_numeral_factor\<close>
+  \<open>K Numeral_Simprocs.divide_cancel_numeral_factor\<close>
 
 simproc_setup ring_eq_cancel_factor
   ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
-  \<open>fn phi => Numeral_Simprocs.eq_cancel_factor\<close>
+  \<open>K Numeral_Simprocs.eq_cancel_factor\<close>
 
 simproc_setup linordered_ring_le_cancel_factor
   ("(l::'a::linordered_idom) * m <= n"
   |"(l::'a::linordered_idom) <= m * n") =
-  \<open>fn phi => Numeral_Simprocs.le_cancel_factor\<close>
+  \<open>K Numeral_Simprocs.le_cancel_factor\<close>
 
 simproc_setup linordered_ring_less_cancel_factor
   ("(l::'a::linordered_idom) * m < n"
   |"(l::'a::linordered_idom) < m * n") =
-  \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
+  \<open>K Numeral_Simprocs.less_cancel_factor\<close>
 
 simproc_setup int_div_cancel_factor
   ("((l::'a::euclidean_semiring_cancel) * m) div n"
   |"(l::'a::euclidean_semiring_cancel) div (m * n)") =
-  \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
+  \<open>K Numeral_Simprocs.div_cancel_factor\<close>
 
 simproc_setup int_mod_cancel_factor
   ("((l::'a::euclidean_semiring_cancel) * m) mod n"
   |"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
-  \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
+  \<open>K Numeral_Simprocs.mod_cancel_factor\<close>
 
 simproc_setup dvd_cancel_factor
   ("((l::'a::idom) * m) dvd n"
   |"(l::'a::idom) dvd (m * n)") =
-  \<open>fn phi => Numeral_Simprocs.dvd_cancel_factor\<close>
+  \<open>K Numeral_Simprocs.dvd_cancel_factor\<close>
 
 simproc_setup divide_cancel_factor
   ("((l::'a::field) * m) / n"
   |"(l::'a::field) / (m * n)") =
-  \<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>
+  \<open>K Numeral_Simprocs.divide_cancel_factor\<close>
 
 ML_file \<open>Tools/nat_numeral_simprocs.ML\<close>
 
 simproc_setup nat_combine_numerals
   ("(i::nat) + j" | "Suc (i + j)") =
-  \<open>fn phi => Nat_Numeral_Simprocs.combine_numerals\<close>
+  \<open>K Nat_Numeral_Simprocs.combine_numerals\<close>
 
 simproc_setup nateq_cancel_numerals
   ("(l::nat) + m = n" | "(l::nat) = m + n" |
    "(l::nat) * m = n" | "(l::nat) = m * n" |
    "Suc m = n" | "m = Suc n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals\<close>
+  \<open>K Nat_Numeral_Simprocs.eq_cancel_numerals\<close>
 
 simproc_setup natless_cancel_numerals
   ("(l::nat) + m < n" | "(l::nat) < m + n" |
    "(l::nat) * m < n" | "(l::nat) < m * n" |
    "Suc m < n" | "m < Suc n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numerals\<close>
+  \<open>K Nat_Numeral_Simprocs.less_cancel_numerals\<close>
 
 simproc_setup natle_cancel_numerals
   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
    "(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
    "Suc m \<le> n" | "m \<le> Suc n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numerals\<close>
+  \<open>K Nat_Numeral_Simprocs.le_cancel_numerals\<close>
 
 simproc_setup natdiff_cancel_numerals
   ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
    "(l::nat) * m - n" | "(l::nat) - m * n" |
    "Suc m - n" | "m - Suc n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals\<close>
+  \<open>K Nat_Numeral_Simprocs.diff_cancel_numerals\<close>
 
 simproc_setup nat_eq_cancel_numeral_factor
   ("(l::nat) * m = n" | "(l::nat) = m * n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>
 
 simproc_setup nat_less_cancel_numeral_factor
   ("(l::nat) * m < n" | "(l::nat) < m * n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>
 
 simproc_setup nat_le_cancel_numeral_factor
   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>
 
 simproc_setup nat_div_cancel_numeral_factor
   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
-  \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>
 
 simproc_setup nat_dvd_cancel_numeral_factor
   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
-  \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>
 
 simproc_setup nat_eq_cancel_factor
   ("(l::nat) * m = n" | "(l::nat) = m * n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.eq_cancel_factor\<close>
 
 simproc_setup nat_less_cancel_factor
   ("(l::nat) * m < n" | "(l::nat) < m * n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.less_cancel_factor\<close>
 
 simproc_setup nat_le_cancel_factor
   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
-  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.le_cancel_factor\<close>
 
 simproc_setup nat_div_cancel_factor
   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
-  \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.div_cancel_factor\<close>
 
 simproc_setup nat_dvd_cancel_factor
   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
-  \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor\<close>
+  \<open>K Nat_Numeral_Simprocs.dvd_cancel_factor\<close>
 
 declaration \<open>
   K (Lin_Arith.add_simprocs
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Product_Type.thy	Tue May 23 21:43:36 2023 +0200
@@ -73,9 +73,9 @@
 \<close>
 
 simproc_setup unit_eq ("x::unit") = \<open>
-  fn _ => fn _ => fn ct =>
+  K (K (fn ct =>
     if HOLogic.is_unit (Thm.term_of ct) then NONE
-    else SOME (mk_meta_eq @{thm unit_eq})
+    else SOME (mk_meta_eq @{thm unit_eq})))
 \<close>
 
 free_constructors case_unit for "()"
@@ -570,9 +570,9 @@
 end;
 \<close>
 simproc_setup case_prod_beta ("case_prod f z") =
-  \<open>fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct))\<close>
 simproc_setup case_prod_eta ("case_prod f") =
-  \<open>fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\<close>
+  \<open>K (fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct))\<close>
 
 lemma case_prod_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
   by (auto simp: fun_eq_iff)
@@ -1326,7 +1326,7 @@
 
 (* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *)
 simproc_setup Collect_mem ("Collect t") = \<open>
-  fn _ => fn ctxt => fn ct =>
+  K (fn ctxt => fn ct =>
     (case Thm.term_of ct of
       S as Const (\<^const_name>\<open>Collect\<close>, Type (\<^type_name>\<open>fun\<close>, [_, T])) $ t =>
         let val (u, _, ps) = HOLogic.strip_ptupleabs t in
@@ -1355,7 +1355,7 @@
                   else NONE)
           | _ => NONE)
         end
-    | _ => NONE)
+    | _ => NONE))
 \<close>
 
 ML_file \<open>Tools/inductive_set.ML\<close>
diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Set.thy	Tue May 23 21:43:36 2023 +0200
@@ -65,13 +65,13 @@
 \<close>
 
 simproc_setup defined_Collect ("{x. P x \<and> Q x}") = \<open>
-  fn _ => Quantifier1.rearrange_Collect
+  K (Quantifier1.rearrange_Collect
     (fn ctxt =>
       resolve_tac ctxt @{thms Collect_cong} 1 THEN
       resolve_tac ctxt @{thms iffI} 1 THEN
       ALLGOALS
         (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
-          DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
+          DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})])))
 \<close>
 
 lemmas CollectE = CollectD [elim_format]
@@ -330,13 +330,11 @@
 \<close>
 
 simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
-  fn _ => Quantifier1.rearrange_Bex
-    (fn ctxt => unfold_tac ctxt @{thms Bex_def})
+  K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
 \<close>
 
 simproc_setup defined_All ("\<forall>x\<in>A. P x \<longrightarrow> Q x") = \<open>
-  fn _ => Quantifier1.rearrange_Ball
-    (fn ctxt => unfold_tac ctxt @{thms Ball_def})
+  K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
 \<close>
 
 lemma ballI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<in>A. P x"
diff -r 2cd7e5518d0d -r 4d9349989d94 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/ZF/OrdQuant.thy	Tue May 23 21:43:36 2023 +0200
@@ -350,13 +350,11 @@
 text \<open>Setting up the one-point-rule simproc\<close>
 
 simproc_setup defined_rex ("\<exists>x[M]. P(x) \<and> Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_Bex
-    (fn ctxt => unfold_tac ctxt @{thms rex_def})
+  K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms rex_def}))
 \<close>
 
 simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_Ball
-    (fn ctxt => unfold_tac ctxt @{thms rall_def})
+  K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms rall_def}))
 \<close>
 
 end
diff -r 2cd7e5518d0d -r 4d9349989d94 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/ZF/pair.thy	Tue May 23 21:43:36 2023 +0200
@@ -19,13 +19,11 @@
 ML \<open>val ZF_ss = simpset_of \<^context>\<close>
 
 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) \<and> Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_Bex
-    (fn ctxt => unfold_tac ctxt @{thms Bex_def})
+  K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
 \<close>
 
 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
-  fn _ => Quantifier1.rearrange_Ball
-    (fn ctxt => unfold_tac ctxt @{thms Ball_def})
+  K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
 \<close>