clarified signature;
clarified modules;

--- a/src/Pure/Pure.thy	Thu Oct 19 21:58:47 2023 +0200
+++ b/src/Pure/Pure.thy	Fri Oct 20 11:03:09 2023 +0200
@@ -333,10 +333,7 @@
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
-    (Simplifier.simproc_setup_parser >> (fn arg =>
-      Context.proof_map
-        (ML_Context.expression (Input.pos_of (#proc arg))
-          (ML_Lex.read "Simplifier.simproc_setup " @ Simplifier.simproc_setup_ml arg))));
+    Simplifier.simproc_setup_command;
 
 in end\<close>
 

--- a/src/Pure/simplifier.ML	Thu Oct 19 21:58:47 2023 +0200
+++ b/src/Pure/simplifier.ML	Fri Oct 20 11:03:09 2023 +0200
@@ -43,12 +43,9 @@
     local_theory -> simproc * local_theory
   val define_simproc_cmd: {passive: bool, name: binding, lhss: string list, proc: morphism -> proc} ->
     local_theory -> simproc * local_theory
-  type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a}
-  type simproc_setup_input = Input.source simproc_setup
-  type simproc_setup_internal = (morphism -> proc) 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: simproc_setup_internal -> simproc
+  val simproc_setup:
+    {passive: bool, name: binding, lhss: string list, proc: morphism -> proc} -> simproc
+  val simproc_setup_command: (local_theory -> local_theory) parser
   val pretty_simpset: bool -> Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
   val prems_of: Proof.context -> thm list
@@ -167,18 +164,14 @@
 
 (* implicit simproc_setup *)
 
-type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a};
-type simproc_setup_input = Input.source simproc_setup;
-type simproc_setup_internal = (morphism -> proc) simproc_setup;
-
-val simproc_setup_parser : simproc_setup_input parser =
+val simproc_setup_parser =
   Scan.optional (Parse.$$$ "passive" >> K true) false --
   Parse.binding --
     (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") --
     (Parse.$$$ "=" |-- Parse.ML_source)
   >> (fn (((a, b), c), d) => {passive = a, name = b, lhss = c, proc = d});
 
-fun simproc_setup_ml ({name, passive, lhss, proc}: simproc_setup_input) =
+fun simproc_setup_ml {name, passive, lhss, proc} =
   ML_Lex.read
     ("{passive = " ^ Bool.toString passive ^
      ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
@@ -189,6 +182,12 @@
   Named_Target.setup_result Raw_Simplifier.transform_simproc
     (define_simproc_cmd args);
 
+val simproc_setup_command =
+  simproc_setup_parser >> (fn args =>
+    Context.proof_map
+      (ML_Context.expression (Input.pos_of (#proc args))
+        (ML_Lex.read "Simplifier.simproc_setup " @ simproc_setup_ml args)));
+
 
 
 (** congruence rule to protect foundational terms of local definitions **)