# HG changeset patch
# User wenzelm
# Date 1697574552 -7200
# Node ID c74fd21af246438eb21ce293b9486ffdff17cbfd
# Parent  2cb027b951886013fdef38aba00aa1f26bee05d3
clarified simproc_setup (passive);

diff -r 2cb027b95188 -r c74fd21af246 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 17 22:25:48 2023 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 17 22:29:12 2023 +0200
@@ -1542,33 +1542,34 @@
 
 ML_file \<open>~~/src/Tools/induction.ML\<close>
 
+simproc_setup swap_induct_false ("induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q") =
+  \<open>fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      _ $ (P as _ $ \<^Const_>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
+        if P <> Q then SOME Drule.swap_prems_eq else NONE
+    | _ => NONE)\<close>
+ (passive)
+
+simproc_setup induct_equal_conj_curry ("induct_conj P Q \<Longrightarrow> PROP R") =
+  \<open>fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      _ $ (_ $ P) $ _ =>
+        let
+          fun is_conj \<^Const_>\<open>induct_conj for P Q\<close> = is_conj P andalso is_conj Q
+            | is_conj \<^Const_>\<open>induct_equal _ for _ _\<close> = true
+            | is_conj \<^Const_>\<open>induct_true\<close> = true
+            | is_conj \<^Const_>\<open>induct_false\<close> = true
+            | is_conj _ = false
+        in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
+      | _ => NONE)\<close>
+ (passive)
+
 declaration \<open>
-  fn _ => Induct.map_simpset (fn ss => ss
-    addsimprocs
-      [Simplifier.make_simproc \<^context> "swap_induct_false"
-        {lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>],
-         proc = fn _ => fn _ => fn ct =>
-          (case Thm.term_of ct of
-            _ $ (P as _ $ \<^Const_>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
-              if P <> Q then SOME Drule.swap_prems_eq else NONE
-          | _ => NONE)},
-       Simplifier.make_simproc \<^context> "induct_equal_conj_curry"
-        {lhss = [\<^term>\<open>induct_conj P Q \<Longrightarrow> PROP R\<close>],
-         proc = fn _ => fn _ => fn ct =>
-          (case Thm.term_of ct of
-            _ $ (_ $ P) $ _ =>
-              let
-                fun is_conj \<^Const_>\<open>induct_conj for P Q\<close> =
-                      is_conj P andalso is_conj Q
-                  | is_conj \<^Const_>\<open>induct_equal _ for _ _\<close> = true
-                  | is_conj \<^Const_>\<open>induct_true\<close> = true
-                  | is_conj \<^Const_>\<open>induct_false\<close> = true
-                  | is_conj _ = false
-              in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
-            | _ => NONE)}]
+  K (Induct.map_simpset (fn ss => ss
+      addsimprocs [\<^simproc>\<open>swap_induct_false\<close>, \<^simproc>\<open>induct_equal_conj_curry\<close>]
     |> Simplifier.set_mksimps (fn ctxt =>
-        Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
-        map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
+      Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
+      map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
 \<close>
 
 text \<open>Pre-simplification of induction and cases rules\<close>
@@ -1933,16 +1934,14 @@
 declare eq_equal [symmetric, code_post]
 declare eq_equal [code]
 
-setup \<open>
-  Code_Preproc.map_pre (fn ctxt =>
-    ctxt addsimprocs
-      [Simplifier.make_simproc \<^context> "equal"
-        {lhss = [\<^term>\<open>HOL.eq\<close>],
-         proc = fn _ => fn _ => fn ct =>
-          (case Thm.term_of ct of
-            Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
-          | _ => NONE)}])
-\<close>
+simproc_setup equal (HOL.eq) =
+  \<open>fn _ => fn _ => fn ct =>
+    (case Thm.term_of ct of
+      Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
+    | _ => NONE)\<close>
+  (passive)
+
+setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>equal\<close>])\<close>
 
 
 subsubsection \<open>Generic code generator foundation\<close>
diff -r 2cb027b95188 -r c74fd21af246 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Oct 17 22:25:48 2023 +0200
+++ b/src/HOL/Product_Type.thy	Tue Oct 17 22:29:12 2023 +0200
@@ -1303,12 +1303,12 @@
 
 ML_file \<open>Tools/set_comprehension_pointfree.ML\<close>
 
-setup \<open>
-  Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
-    [Simplifier.make_simproc \<^context> "set comprehension"
-      {lhss = [\<^term>\<open>Collect P\<close>],
-       proc = K Set_Comprehension_Pointfree.code_simproc}])
-\<close>
+simproc_setup set_comprehension ("Collect P") =
+  \<open>K Set_Comprehension_Pointfree.code_simproc\<close>
+  (passive)
+
+setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>set_comprehension\<close>])\<close>
+
 
 subsection \<open>Lemmas about disjointness\<close>