# HG changeset patch
# User wenzelm
# Date 1697745527 -7200
# Node ID 88593174aef5ef77dfbeec6fd9281d3d68389f99
# Parent  42ae6e0ecfd46f7ab60bcd21b779d4f7b64bc2f2
tuned signature;

diff -r 42ae6e0ecfd4 -r 88593174aef5 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Oct 19 21:38:09 2023 +0200
+++ b/src/Pure/simplifier.ML	Thu Oct 19 21:58:47 2023 +0200
@@ -39,9 +39,10 @@
   val the_simproc: Proof.context -> string -> simproc
   val make_simproc: Proof.context -> string ->
     {lhss: term list, proc: morphism -> proc} -> simproc
-  type 'a simproc_spec = {passive: bool, lhss: 'a list, proc: morphism -> proc}
-  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
+  val define_simproc: {passive: bool, name: binding, lhss: term list, proc: morphism -> proc} ->
+    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
@@ -136,26 +137,21 @@
       {lhss = lhss', proc = Morphism.entity proc}
   end;
 
-type 'a simproc_spec =
- {passive: bool,
-  lhss: 'a list,
-  proc: morphism -> proc};
-
 local
 
-fun def_simproc prep b {passive, lhss, proc} lthy =
+fun def_simproc prep {passive, name, lhss, proc} lthy =
   let
     val simproc0 =
-      make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
+      make_simproc lthy (Local_Theory.full_name lthy name) {lhss = prep lthy lhss, proc = proc};
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of b}
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of name}
       (fn phi => fn context =>
         let
-          val b' = Morphism.binding phi b;
+          val name' = Morphism.binding phi name;
           val simproc' = simproc0 |> transform_simproc phi |> trim_context_simproc;
         in
           context
-          |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
+          |> Simprocs.map (#2 o Name_Space.define context true (name', simproc'))
           |> not passive ? map_ss (fn ctxt => ctxt addsimprocs [simproc'])
         end)
     |> pair simproc0
@@ -189,9 +185,9 @@
      ", lhss = " ^ ML_Syntax.print_strings lhss ^
      ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}";
 
-fun simproc_setup ({name, lhss, passive, proc}: simproc_setup_internal) =
+fun simproc_setup args =
   Named_Target.setup_result Raw_Simplifier.transform_simproc
-    (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc});
+    (define_simproc_cmd args);