clarified signature;
clarified modules;

--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 18 16:29:24 2023 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 18 22:09:25 2023 +0200
@@ -17,7 +17,6 @@
   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: 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
@@ -134,14 +133,6 @@
   |> Context.proof_map;
 
 
-(* simprocs *)
-
-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 *)
 
 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));

--- a/src/Pure/Pure.thy	Wed Oct 18 16:29:24 2023 +0200
+++ b/src/Pure/Pure.thy	Wed Oct 18 22:09:25 2023 +0200
@@ -333,12 +333,10 @@
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
-    (Parse.binding --
-      (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close>) --
-      (\<^keyword>\<open>=\<close> |-- Parse.ML_source) --
-      Parse.opt_keyword "passive"
-    >> (fn (((name, lhss), proc), passive) =>
-        Isar_Cmd.simproc_setup {name = name, lhss = lhss, passive = passive, proc = proc}));
+    (Simplifier.simproc_setup_parser >> (fn arg =>
+      Context.proof_map
+        (ML_Context.expression (Input.pos_of (#proc arg))
+          (ML_Lex.read "Simplifier.simproc_setup_local " @ Simplifier.simproc_setup_ml arg))));
 
 in end\<close>
 

--- a/src/Pure/simplifier.ML	Wed Oct 18 16:29:24 2023 +0200
+++ b/src/Pure/simplifier.ML	Wed Oct 18 22:09:25 2023 +0200
@@ -44,11 +44,12 @@
   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
+  type simproc_setup_input = Input.source simproc_setup
+  type simproc_setup_internal = (morphism -> Proof.context -> cterm -> thm option) simproc_setup
+  val simproc_setup_parser: Input.source simproc_setup parser
   val simproc_setup_ml: Input.source simproc_setup -> ML_Lex.token Antiquote.antiquote list
+  val simproc_setup_local: simproc_setup_internal -> simproc
+  val simproc_setup_global: simproc_setup_internal -> simproc
   val pretty_simpset: bool -> Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
   val prems_of: Proof.context -> thm list
@@ -173,22 +174,30 @@
 (* 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});
+type simproc_setup_input = Input.source simproc_setup;
+type simproc_setup_internal = (morphism -> Proof.context -> cterm -> thm option) simproc_setup;
 
-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});
+val simproc_setup_parser : simproc_setup_input parser =
+  Parse.binding -- (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") --
+    (Parse.$$$ "=" |-- Parse.ML_source) -- Parse.opt_keyword "passive"
+  >> (fn (((name, lhss), proc), passive) =>
+        {name = name, lhss = lhss, passive = passive, proc = proc});
 
-fun simproc_setup_ml {name, lhss, passive, proc} =
+fun simproc_setup_ml ({name, lhss, passive, proc}: simproc_setup_input) =
   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 ")}";
 
+fun simproc_setup_local ({name, lhss, passive, proc}: simproc_setup_internal) =
+  Theory.local_setup_result
+    (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc});
+
+fun simproc_setup_global ({name, lhss, passive, proc}: simproc_setup_internal) =
+  Named_Target.global_setup_result Raw_Simplifier.transform_simproc
+    (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc});
+
 
 
 (** congruence rule to protect foundational terms of local definitions **)