tuned signature;

--- a/src/Pure/simplifier.ML	Sat Oct 21 11:24:34 2023 +0200
+++ b/src/Pure/simplifier.ML	Sat Oct 21 11:34:37 2023 +0200
@@ -39,12 +39,10 @@
   val the_simproc: Proof.context -> string -> simproc
   val make_simproc: Proof.context -> string ->
     {lhss: term list, proc: morphism -> proc} -> simproc
-  val define_simproc: {passive: bool, name: binding, lhss: term list, proc: morphism -> proc} ->
-    local_theory -> simproc * local_theory
-  val simproc_setup:
-    {passive: bool, name: binding, lhss: term list, proc: morphism -> proc} -> simproc
-  val simproc_setup_cmd:
-    {passive: bool, name: binding, lhss: string list, proc: morphism -> proc} -> simproc
+  type 'a simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: morphism -> proc}
+  val define_simproc: term simproc_spec -> local_theory -> simproc * local_theory
+  val simproc_setup: term simproc_spec -> simproc
+  val simproc_setup_cmd: string simproc_spec -> 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
@@ -134,6 +132,8 @@
       {lhss = lhss', proc = Morphism.entity proc}
   end;
 
+type 'a simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: morphism -> proc};
+
 fun define_simproc {passive, name, lhss, proc} lthy =
   let
     val simproc0 =