more standard simproc_setup using ML antiquotation;

--- a/src/HOL/Statespace/state_fun.ML	Sat Oct 21 00:13:12 2023 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Sat Oct 21 00:25:40 2023 +0200
@@ -54,9 +54,8 @@
 in
 
 val lazy_conj_simproc =
-  Simplifier.make_simproc \<^context> "lazy_conj_simp"
-   {lhss = [\<^term>\<open>P & Q\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+  \<^simproc_setup>\<open>passive lazy_conj_simp ("P & Q") =
+    \<open>fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         Const (\<^const_name>\<open>HOL.conj\<close>,_) $ P $ Q =>
           let
@@ -75,7 +74,7 @@
                 else SOME (conj_cong OF [P_P', Q_Q'])
               end
            end
-      | _ => NONE)};
+      | _ => NONE)\<close>\<close>;
 
 fun string_eq_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt
@@ -122,9 +121,8 @@
 val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)));
 
 val lookup_simproc =
-  Simplifier.make_simproc \<^context> "lookup_simp"
-   {lhss = [\<^term>\<open>lookup d n (update d' c m v s)\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+  \<^simproc_setup>\<open>passive lookup_simp ("lookup d n (update d' c m v s)") =
+    \<open>fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of (Const (\<^const_name>\<open>StateFun.lookup\<close>, lT) $ destr $ n $
                    (s as Const (\<^const_name>\<open>StateFun.update\<close>, uT) $ _ $ _ $ _ $ _ $ _)) =>
         (let
@@ -166,8 +164,7 @@
           else SOME thm
         end
         handle Option.Option => NONE)
-      | _ => NONE)};
-
+      | _ => NONE)\<close>\<close>;
 
 local
 
@@ -182,9 +179,8 @@
 in
 
 val update_simproc =
-  Simplifier.make_simproc \<^context> "update_simp"
-   {lhss = [\<^term>\<open>update d c n v s\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+  \<^simproc_setup>\<open>passive update_simp ("update d c n v s") =
+    \<open>fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         Const (\<^const_name>\<open>StateFun.update\<close>, uT) $ _ $ _ $ _ $ _ $ _ =>
           let
@@ -271,7 +267,7 @@
                 in SOME (Thm.transitive eq1 eq2) end
             | _ => NONE)
           end
-      | _ => NONE)};
+      | _ => NONE)\<close>\<close>;
 
 end;
 
@@ -287,9 +283,8 @@
 in
 
 val ex_lookup_eq_simproc =
-  Simplifier.make_simproc \<^context> "ex_lookup_eq_simproc"
-   {lhss = [\<^term>\<open>Ex t\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+  \<^simproc_setup>\<open>passive ex_lookup_eq ("Ex t") =
+    \<open>fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
@@ -336,7 +331,7 @@
               val thm' = if swap then swap_ex_eq OF [thm] else thm
             in SOME thm' end handle TERM _ => NONE)
         | _ => NONE)
-      end handle Option.Option => NONE};
+      end handle Option.Option => NONE\<close>\<close>;
 
 end;
 

--- a/src/HOL/Statespace/state_space.ML	Sat Oct 21 00:13:12 2023 +0200
+++ b/src/HOL/Statespace/state_space.ML	Sat Oct 21 00:25:40 2023 +0200
@@ -293,14 +293,13 @@
 val distinctNameSolver = mk_solver "distinctNameSolver" distinctTree_tac;
 
 val distinct_simproc =
-  Simplifier.make_simproc \<^context> "StateSpace.distinct_simproc"
-   {lhss = [\<^term>\<open>x = y\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+  \<^simproc_setup>\<open>passive distinct_simproc ("x = y") =
+    \<open>fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         Const (\<^const_name>\<open>HOL.eq\<close>,_) $ (x as Free _) $ (y as Free _) =>
           Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
             (neq_x_y ctxt x y)
-      | _ => NONE)};
+      | _ => NONE)\<close>\<close>;
 
 fun interprete_parent name dist_thm_name parent_expr thy =
   let