clarified signature: more concise simproc setup in ML;

--- a/src/HOL/Tools/record.ML	Wed Oct 18 15:13:52 2023 +0200
+++ b/src/HOL/Tools/record.ML	Wed Oct 18 16:29:24 2023 +0200
@@ -1060,65 +1060,65 @@
   - If X is a more-selector we have to make sure that S is not in the updated
     subrecord.
 *)
-val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>select_update\<close>
-   {lhss = [\<^term>\<open>x::'a::{}\<close>],
-    passive = false,
-    proc = fn _ => fn ctxt => fn ct =>
-      let
-        val thy = Proof_Context.theory_of ctxt;
-        val t = Thm.term_of ct;
-      in
-        (case t of
-          (sel as Const (s, Type (_, [_, rangeS]))) $
-              ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
-            if is_selector thy s andalso is_some (get_updates thy u) then
-              let
-                val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
-
-                fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
-                      (case Symtab.lookup updates u of
-                        NONE => NONE
-                      | SOME u_name =>
-                          if u_name = s then
-                            (case mk_eq_terms r of
-                              NONE =>
-                                let
-                                  val rv = ("r", rT);
-                                  val rb = Bound 0;
-                                  val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
-                                in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
-                            | SOME (trm, trm', vars) =>
-                                let
-                                  val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
-                                in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
-                          else if has_field extfields u_name rangeS orelse
-                            has_field extfields s (domain_type kT) then NONE
-                          else
-                            (case mk_eq_terms r of
-                              SOME (trm, trm', vars) =>
-                                let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
-                                in SOME (upd $ kb $ trm, trm', kv :: vars) end
-                            | NONE =>
-                                let
-                                  val rv = ("r", rT);
-                                  val rb = Bound 0;
-                                  val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
-                                in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
-                  | mk_eq_terms _ = NONE;
-              in
-                (case mk_eq_terms (upd $ k $ r) of
-                  SOME (trm, trm', vars) =>
-                    SOME
-                      (prove_unfold_defs thy [] [] []
-                        (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
-                | NONE => NONE)
-              end
-            else NONE
-        | _ => NONE)
-      end});
+
+fun select_update_proc ctxt ct =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val t = Thm.term_of ct;
+  in
+    (case t of
+      (sel as Const (s, Type (_, [_, rangeS]))) $
+          ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
+        if is_selector thy s andalso is_some (get_updates thy u) then
+          let
+            val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
+
+            fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
+                  (case Symtab.lookup updates u of
+                    NONE => NONE
+                  | SOME u_name =>
+                      if u_name = s then
+                        (case mk_eq_terms r of
+                          NONE =>
+                            let
+                              val rv = ("r", rT);
+                              val rb = Bound 0;
+                              val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
+                            in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
+                        | SOME (trm, trm', vars) =>
+                            let
+                              val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
+                            in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
+                      else if has_field extfields u_name rangeS orelse
+                        has_field extfields s (domain_type kT) then NONE
+                      else
+                        (case mk_eq_terms r of
+                          SOME (trm, trm', vars) =>
+                            let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
+                            in SOME (upd $ kb $ trm, trm', kv :: vars) end
+                        | NONE =>
+                            let
+                              val rv = ("r", rT);
+                              val rb = Bound 0;
+                              val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
+                            in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
+              | mk_eq_terms _ = NONE;
+          in
+            (case mk_eq_terms (upd $ k $ r) of
+              SOME (trm, trm', vars) =>
+                SOME
+                  (prove_unfold_defs thy [] [] []
+                    (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
+            | NONE => NONE)
+          end
+        else NONE
+    | _ => NONE)
+  end;
 
 val simproc =
-  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none));
+  Simplifier.simproc_setup_global
+   {name = \<^binding>\<open>select_update\<close>, lhss = ["x::'a::{}"], proc = K select_update_proc,
+     passive = false};
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
@@ -1165,128 +1165,127 @@
   In both cases "more" updates complicate matters: for this reason
   we omit considering further updates if doing so would introduce
   both a more update and an update to a field within it.*)
-val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>update\<close>
-   {lhss = [\<^term>\<open>x::'a::{}\<close>],
-    passive = false,
-    proc = fn _ => fn ctxt => fn ct =>
+
+fun upd_proc ctxt ct =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val t = Thm.term_of ct;
+    (*We can use more-updators with other updators as long
+      as none of the other updators go deeper than any more
+      updator. min here is the depth of the deepest other
+      updator, max the depth of the shallowest more updator.*)
+    fun include_depth (dep, true) (min, max) =
+          if min <= dep
+          then SOME (min, if dep <= max orelse max = ~1 then dep else max)
+          else NONE
+      | include_depth (dep, false) (min, max) =
+          if dep <= max orelse max = ~1
+          then SOME (if min <= dep then dep else min, max)
+          else NONE;
+
+    fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
+          (case get_update_details u thy of
+            SOME (s, dep, ismore) =>
+              (case include_depth (dep, ismore) (min, max) of
+                SOME (min', max') =>
+                  let val (us, bs, _) = getupdseq tm min' max'
+                  in ((upd, s, f) :: us, bs, fastype_of term) end
+              | NONE => ([], term, HOLogic.unitT))
+          | NONE => ([], term, HOLogic.unitT))
+      | getupdseq term _ _ = ([], term, HOLogic.unitT);
+
+    val (upds, base, baseT) = getupdseq t 0 ~1;
+    val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds
+    val upd_ord = rev_order o fast_string_ord o apply2 #2
+    val (upds, commuted) =
+      if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord orig_upds) then
+         (sort upd_ord orig_upds, true)
+      else
+         (orig_upds, false)
+
+    fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
+          if s = s' andalso null (loose_bnos tm')
+            andalso subst_bound (HOLogic.unit, tm') = tm
+          then (true, Abs (n, T, Const (s', T') $ Bound 1))
+          else (false, HOLogic.unit)
+      | is_upd_noop _ _ _ = (false, HOLogic.unit);
+
+    fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
       let
-        val thy = Proof_Context.theory_of ctxt;
-        val t = Thm.term_of ct;
-        (*We can use more-updators with other updators as long
-          as none of the other updators go deeper than any more
-          updator. min here is the depth of the deepest other
-          updator, max the depth of the shallowest more updator.*)
-        fun include_depth (dep, true) (min, max) =
-              if min <= dep
-              then SOME (min, if dep <= max orelse max = ~1 then dep else max)
-              else NONE
-          | include_depth (dep, false) (min, max) =
-              if dep <= max orelse max = ~1
-              then SOME (if min <= dep then dep else min, max)
-              else NONE;
-
-        fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
-              (case get_update_details u thy of
-                SOME (s, dep, ismore) =>
-                  (case include_depth (dep, ismore) (min, max) of
-                    SOME (min', max') =>
-                      let val (us, bs, _) = getupdseq tm min' max'
-                      in ((upd, s, f) :: us, bs, fastype_of term) end
-                  | NONE => ([], term, HOLogic.unitT))
-              | NONE => ([], term, HOLogic.unitT))
-          | getupdseq term _ _ = ([], term, HOLogic.unitT);
-
-        val (upds, base, baseT) = getupdseq t 0 ~1;
-        val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds
-        val upd_ord = rev_order o fast_string_ord o apply2 #2
-        val (upds, commuted) =
-          if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord orig_upds) then
-             (sort upd_ord orig_upds, true)
-          else
-             (orig_upds, false)
-
-        fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
-              if s = s' andalso null (loose_bnos tm')
-                andalso subst_bound (HOLogic.unit, tm') = tm
-              then (true, Abs (n, T, Const (s', T') $ Bound 1))
-              else (false, HOLogic.unit)
-          | is_upd_noop _ _ _ = (false, HOLogic.unit);
-
-        fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
+        val ss = get_sel_upd_defs thy;
+        val uathm = get_upd_acc_cong_thm upd acc thy ss;
+      in
+       [Drule.export_without_context (uathm RS updacc_noopE),
+        Drule.export_without_context (uathm RS updacc_noop_compE)]
+      end;
+
+    (*If f is constant then (f o g) = f.  We know that K_skeleton
+      only returns constant abstractions thus when we see an
+      abstraction we can discard inner updates.*)
+    fun add_upd (f as Abs _) _ = [f]
+      | add_upd f fs = (f :: fs);
+
+    (*mk_updterm returns
+      (orig-term-skeleton-update list , simplified-skeleton,
+        variables, duplicate-updates, simp-flag, noop-simps)
+
+      where duplicate-updates is a table used to pass upward
+      the list of update functions which can be composed
+      into an update above them, simp-flag indicates whether
+      any simplification was achieved, and noop-simps are
+      used for eliminating case (2) defined above*)
+    fun mk_updterm ((upd as Const (u, T), s, f, i) :: upds) above term =
           let
-            val ss = get_sel_upd_defs thy;
-            val uathm = get_upd_acc_cong_thm upd acc thy ss;
+            val (lhs_upds, rhs, vars, dups, simp, noops) =
+              mk_updterm upds (Symtab.update (u, ()) above) term;
+            val (fvar, skelf) =
+              K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
+            val (isnoop, skelf') = is_upd_noop s f term;
+            val funT = domain_type T;
+            fun mk_comp_local (f, f') =
+              Const (\<^const_name>\<open>Fun.comp\<close>, funT --> funT --> funT) $ f $ f';
           in
-           [Drule.export_without_context (uathm RS updacc_noopE),
-            Drule.export_without_context (uathm RS updacc_noop_compE)]
-          end;
-
-        (*If f is constant then (f o g) = f.  We know that K_skeleton
-          only returns constant abstractions thus when we see an
-          abstraction we can discard inner updates.*)
-        fun add_upd (f as Abs _) _ = [f]
-          | add_upd f fs = (f :: fs);
-
-        (*mk_updterm returns
-          (orig-term-skeleton-update list , simplified-skeleton,
-            variables, duplicate-updates, simp-flag, noop-simps)
-
-          where duplicate-updates is a table used to pass upward
-          the list of update functions which can be composed
-          into an update above them, simp-flag indicates whether
-          any simplification was achieved, and noop-simps are
-          used for eliminating case (2) defined above*)
-        fun mk_updterm ((upd as Const (u, T), s, f, i) :: upds) above term =
-              let
-                val (lhs_upds, rhs, vars, dups, simp, noops) =
-                  mk_updterm upds (Symtab.update (u, ()) above) term;
-                val (fvar, skelf) =
-                  K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
-                val (isnoop, skelf') = is_upd_noop s f term;
-                val funT = domain_type T;
-                fun mk_comp_local (f, f') =
-                  Const (\<^const_name>\<open>Fun.comp\<close>, funT --> funT --> funT) $ f $ f';
-              in
-                if isnoop then
-                  ((upd $ skelf', i)::lhs_upds, rhs, vars,
-                    Symtab.update (u, []) dups, true,
-                    if Symtab.defined noops u then noops
-                    else Symtab.update (u, get_noop_simps upd skelf') noops)
-                else if Symtab.defined above u then
-                  ((upd $ skelf, i)::lhs_upds, rhs, fvar :: vars,
-                    Symtab.map_default (u, []) (add_upd skelf) dups,
-                    true, noops)
-                else
-                  (case Symtab.lookup dups u of
-                    SOME fs =>
-                     ((upd $ skelf, i)::lhs_upds,
-                      upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
-                      fvar :: vars, dups, true, noops)
-                  | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
-              end
-          | mk_updterm [] _ _ =
-              ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
-          | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us);
-
-        val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
-        val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd)
-        val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds
-        (* Note that the simplifier works bottom up. So all nested updates are already
-           normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be
-           inserted at its place inside the sorted nested updates. The necessary swaps can be
-           expressed via 'upd_funs' by replicating the outer update at the designated position: *)
-        val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1
-        val noops' = maps snd (Symtab.dest noops);
-      in
-        if simp orelse commuted then
-          SOME
-            (prove_unfold_defs thy upd_funs noops' [simproc]
-              (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
-        else NONE
-      end});
+            if isnoop then
+              ((upd $ skelf', i)::lhs_upds, rhs, vars,
+                Symtab.update (u, []) dups, true,
+                if Symtab.defined noops u then noops
+                else Symtab.update (u, get_noop_simps upd skelf') noops)
+            else if Symtab.defined above u then
+              ((upd $ skelf, i)::lhs_upds, rhs, fvar :: vars,
+                Symtab.map_default (u, []) (add_upd skelf) dups,
+                true, noops)
+            else
+              (case Symtab.lookup dups u of
+                SOME fs =>
+                 ((upd $ skelf, i)::lhs_upds,
+                  upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
+                  fvar :: vars, dups, true, noops)
+              | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
+          end
+      | mk_updterm [] _ _ =
+          ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
+      | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us);
+
+    val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
+    val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd)
+    val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds
+    (* Note that the simplifier works bottom up. So all nested updates are already
+       normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be
+       inserted at its place inside the sorted nested updates. The necessary swaps can be
+       expressed via 'upd_funs' by replicating the outer update at the designated position: *)
+    val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1
+    val noops' = maps snd (Symtab.dest noops);
+  in
+    if simp orelse commuted then
+      SOME
+        (prove_unfold_defs thy upd_funs noops' [simproc]
+          (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
+    else NONE
+  end;
 
 val upd_simproc =
-  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none));
+  Simplifier.simproc_setup_global
+    {name = \<^binding>\<open>update\<close>, lhss = ["x::'a::{}"], proc = K upd_proc, passive = false};
 
 end;
 
@@ -1306,22 +1305,20 @@
  Complexity: #components * #updates     #updates
 *)
 
-val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>eq\<close>
-   {lhss = [\<^term>\<open>r = s\<close>],
-    passive = false,
-    proc = fn _ => fn ctxt => fn ct =>
-      (case Thm.term_of ct of
-        \<^Const_>\<open>HOL.eq T for _ _\<close> =>
-          (case rec_id ~1 T of
-            "" => NONE
-          | name =>
-              (case get_equalities (Proof_Context.theory_of ctxt) name of
-                NONE => NONE
-              | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
-      | _ => NONE)});
+fun eq_proc ctxt ct =
+  (case Thm.term_of ct of
+    \<^Const_>\<open>HOL.eq T for _ _\<close> =>
+      (case rec_id ~1 T of
+        "" => NONE
+      | name =>
+          (case get_equalities (Proof_Context.theory_of ctxt) name of
+            NONE => NONE
+          | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
+  | _ => NONE);
 
 val eq_simproc =
-  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none));
+  Simplifier.simproc_setup_global
+    {name = \<^binding>\<open>eq\<close>, lhss = ["r = s"], proc = K eq_proc, passive = false};
 
 
 (* split_simproc *)
@@ -1360,51 +1357,47 @@
           else NONE
       | _ => NONE)};
 
-val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>ex_sel_eq\<close>
-   {lhss = [\<^term>\<open>Ex t\<close>],
-    passive = false,
-    proc = fn _ => fn ctxt => fn ct =>
-      let
-        val thy = Proof_Context.theory_of ctxt;
-        val t = Thm.term_of ct;
-        fun mkeq (lr, T, (sel, Tsel), x) i =
-          if is_selector thy sel then
-            let
-              val x' =
-                if not (Term.is_dependent x)
-                then Free ("x" ^ string_of_int i, range_type Tsel)
-                else raise TERM ("", [x]);
-              val sel' = Const (sel, Tsel) $ Bound 0;
-              val (l, r) = if lr then (sel', x') else (x', sel');
-            in \<^Const>\<open>HOL.eq T for l r\<close> end
-          else raise TERM ("", [Const (sel, Tsel)]);
-
-        fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) =
-              (true, T, (sel, Tsel), X)
-          | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) =
-              (false, T, (sel, Tsel), X)
-          | dest_sel_eq _ = raise TERM ("", []);
-      in
-        (case t of
-          \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> =>
-           (let
-             val eq = mkeq (dest_sel_eq t) 0;
-             val prop =
-               Logic.list_all ([("r", T)],
-                 Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\<close>));
-            in
-              SOME (Goal.prove_sorry_global thy [] [] prop
-                (fn {context = ctxt', ...} =>
-                  simp_tac (put_simpset (get_simpset thy) ctxt'
-                    addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
-            end handle TERM _ => NONE)
-        | _ => NONE)
-      end});
+fun ex_sel_eq_proc ctxt ct =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val t = Thm.term_of ct;
+    fun mkeq (lr, T, (sel, Tsel), x) i =
+      if is_selector thy sel then
+        let
+          val x' =
+            if not (Term.is_dependent x)
+            then Free ("x" ^ string_of_int i, range_type Tsel)
+            else raise TERM ("", [x]);
+          val sel' = Const (sel, Tsel) $ Bound 0;
+          val (l, r) = if lr then (sel', x') else (x', sel');
+        in \<^Const>\<open>HOL.eq T for l r\<close> end
+      else raise TERM ("", [Const (sel, Tsel)]);
+
+    fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) =
+          (true, T, (sel, Tsel), X)
+      | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) =
+          (false, T, (sel, Tsel), X)
+      | dest_sel_eq _ = raise TERM ("", []);
+  in
+    (case t of
+      \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> =>
+       (let
+         val eq = mkeq (dest_sel_eq t) 0;
+         val prop =
+           Logic.list_all ([("r", T)],
+             Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\<close>));
+        in
+          SOME (Goal.prove_sorry_global thy [] [] prop
+            (fn {context = ctxt', ...} =>
+              simp_tac (put_simpset (get_simpset thy) ctxt'
+                addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
+        end handle TERM _ => NONE)
+    | _ => NONE)
+  end;
 
 val ex_sel_eq_simproc =
-  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none));
-
-val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs [ex_sel_eq_simproc]));
+  Simplifier.simproc_setup_global
+    {name = \<^binding>\<open>ex_sel_eq\<close>, lhss = ["Ex t"], proc = K ex_sel_eq_proc, passive = true};
 
 
 (* split_simp_tac *)

--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 18 15:13:52 2023 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 18 16:29:24 2023 +0200
@@ -17,8 +17,7 @@
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val oracle: bstring * Position.range -> Input.source -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
-  val simproc_setup: string * Position.T -> string list -> Input.source -> bool ->
-    local_theory -> local_theory
+  val simproc_setup: Input.source Simplifier.simproc_setup -> local_theory -> local_theory
   val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text_range * Method.text_range option ->
     Toplevel.transition -> Toplevel.transition
@@ -137,14 +136,10 @@
 
 (* simprocs *)
 
-fun simproc_setup name lhss source passive =
-  ML_Context.expression (Input.pos_of source)
-    (ML_Lex.read
-      ("Theory.local_setup (Simplifier.define_simproc_cmd (" ^
-        ML_Syntax.make_binding name ^ ") {lhss = " ^ ML_Syntax.print_strings lhss ^
-        ", passive = " ^ Bool.toString passive ^
-        ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})")
-  |> Context.proof_map;
+fun simproc_setup arg =
+  Context.proof_map
+    (ML_Context.expression (Input.pos_of (#proc arg))
+      (ML_Lex.read "Simplifier.simproc_setup_local " @ Simplifier.simproc_setup_ml arg));
 
 
 (* local endings *)

--- a/src/Pure/Pure.thy	Wed Oct 18 15:13:52 2023 +0200
+++ b/src/Pure/Pure.thy	Wed Oct 18 16:29:24 2023 +0200
@@ -333,11 +333,12 @@
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
-    (Parse.name_position --
+    (Parse.binding --
       (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close>) --
       (\<^keyword>\<open>=\<close> |-- Parse.ML_source) --
       Parse.opt_keyword "passive"
-    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
+    >> (fn (((name, lhss), proc), passive) =>
+        Isar_Cmd.simproc_setup {name = name, lhss = lhss, passive = passive, proc = proc}));
 
 in end\<close>
 

--- a/src/Pure/ex/Def.thy	Wed Oct 18 15:13:52 2023 +0200
+++ b/src/Pure/ex/Def.thy	Wed Oct 18 16:29:24 2023 +0200
@@ -66,9 +66,8 @@
 (* simproc setup *)
 
 val _ =
-  Named_Target.global_setup
-    (Simplifier.define_simproc \<^binding>\<open>expand_def\<close>
-      {lhss = [Free ("x", TFree ("'a", []))], passive = false, proc = K get_def});
+  Simplifier.simproc_setup_global
+    {name = \<^binding>\<open>expand_def\<close>, lhss = ["x::'a"], passive = false, proc = K get_def};
 
 
 (* Isar command *)

--- a/src/Pure/simplifier.ML	Wed Oct 18 15:13:52 2023 +0200
+++ b/src/Pure/simplifier.ML	Wed Oct 18 16:29:24 2023 +0200
@@ -41,8 +41,14 @@
     {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
   type 'a simproc_spec =
     {lhss: 'a list, passive: bool, proc: morphism -> Proof.context -> cterm -> thm option}
-  val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
-  val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
+  val define_simproc: binding -> term simproc_spec -> local_theory -> simproc * local_theory
+  val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> simproc * local_theory
+  type 'a simproc_setup = {name: binding, lhss: string list, passive: bool, proc: 'a}
+  val simproc_setup_local:
+    (morphism -> Proof.context -> cterm -> thm option) simproc_setup -> simproc
+  val simproc_setup_global:
+    (morphism -> Proof.context -> cterm -> thm option) simproc_setup -> simproc
+  val simproc_setup_ml: Input.source simproc_setup -> ML_Lex.token Antiquote.antiquote list
   val pretty_simpset: bool -> Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
   val prems_of: Proof.context -> thm list
@@ -153,6 +159,7 @@
           |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
           |> not passive ? map_ss (fn ctxt => ctxt addsimprocs [simproc'])
         end)
+    |> pair simproc0
   end;
 
 in
@@ -163,6 +170,27 @@
 end;
 
 
+(* implicit simproc_setup *)
+
+type 'a simproc_setup = {name: binding, lhss: string list, passive: bool, proc: 'a};
+
+fun simproc_setup_local {name, lhss, passive, proc} =
+  Theory.local_setup_result
+    (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc});
+
+fun simproc_setup_global {name, lhss, passive, proc} =
+  Named_Target.global_setup_result Raw_Simplifier.transform_simproc
+    (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc});
+
+fun simproc_setup_ml {name, lhss, passive, proc} =
+  ML_Lex.read
+    ("{name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
+     ", lhss = " ^ ML_Syntax.print_strings lhss ^
+     ", passive = " ^ Bool.toString passive ^
+     ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}";
+
+
+
 (** congruence rule to protect foundational terms of local definitions **)
 
 local