tuned signature;

--- a/src/HOL/Tools/record.ML	Fri May 26 13:19:49 2023 +0200
+++ b/src/HOL/Tools/record.ML	Sat May 27 13:29:13 2023 +0200
@@ -1116,9 +1116,8 @@
         | _ => NONE)
       end}));
 
-val simproc_name =
-  Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none);
-val simproc = Simplifier.the_simproc (Context.the_local_context ()) simproc_name;
+val simproc =
+  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none));
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
@@ -1284,9 +1283,8 @@
         else NONE
       end}));
 
-val upd_simproc_name =
-  Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none);
-val upd_simproc = Simplifier.the_simproc (Context.the_local_context ()) upd_simproc_name;
+val upd_simproc =
+  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none));
 
 end;
 
@@ -1319,8 +1317,9 @@
               | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
       | _ => NONE)}));
 
-val eq_simproc_name = Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none);
-val eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) eq_simproc_name;
+val eq_simproc =
+  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none));
+
 
 (* split_simproc *)
 
@@ -1398,9 +1397,9 @@
         | _ => NONE)
       end}));
 
-val ex_sel_eq_simproc_name =
-  Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none);
-val ex_sel_eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) ex_sel_eq_simproc_name;
+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]));
 
 

--- a/src/Pure/simplifier.ML	Fri May 26 13:19:49 2023 +0200
+++ b/src/Pure/simplifier.ML	Sat May 27 13:29:13 2023 +0200
@@ -35,7 +35,7 @@
   val simp_flip: attribute
   val cong_add: attribute
   val cong_del: attribute
-  val check_simproc: Proof.context -> xstring * Position.T -> string
+  val check_simproc: Proof.context -> xstring * Position.T -> string * simproc
   val the_simproc: Proof.context -> string -> simproc
   type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
   val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
@@ -109,14 +109,13 @@
 
 val get_simprocs = Simprocs.get o Context.Proof;
 
-fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
 val the_simproc = Name_Space.get o get_simprocs;
+fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt);
 
 val _ = Theory.setup
   (ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
-    (Args.context -- Scan.lift Parse.embedded_position
-      >> (fn (ctxt, name) =>
-        "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
+    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, name) =>
+      "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (#1 (check_simproc ctxt name)))));
 
 
 (* define simprocs *)
@@ -319,7 +318,7 @@
 
 val simproc_att =
   (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
-    Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
+    Scan.repeat1 (Scan.lift (Args.named_attribute (decl o #2 o check_simproc ctxt))))
   >> (fn atts => Thm.declaration_attribute (fn th =>
         fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));