# HG changeset patch
# User wenzelm
# Date 1697725877 -7200
# Node ID 807b249f1061a37c007bfe395a8400f4f75a6b70
# Parent  200daaab2578f22260926f72a58a042e8035f0a0
clarified syntax and order of parameters;

diff -r 200daaab2578 -r 807b249f1061 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Oct 19 11:30:16 2023 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 19 16:31:17 2023 +0200
@@ -1542,15 +1542,14 @@
 
 ML_file \<open>~~/src/Tools/induction.ML\<close>
 
-simproc_setup swap_induct_false ("induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q") =
+simproc_setup passive 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") =
+
+simproc_setup passive induct_equal_conj_curry ("induct_conj P Q \<Longrightarrow> PROP R") =
   \<open>fn _ => fn _ => fn ct =>
     (case Thm.term_of ct of
       _ $ (_ $ P) $ _ =>
@@ -1562,7 +1561,6 @@
             | is_conj _ = false
         in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
       | _ => NONE)\<close>
- (passive)
 
 declaration \<open>
   K (Induct.map_simpset (fn ss => ss
@@ -1934,12 +1932,11 @@
 declare eq_equal [symmetric, code_post]
 declare eq_equal [code]
 
-simproc_setup equal (HOL.eq) =
+simproc_setup passive 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>
 
diff -r 200daaab2578 -r 807b249f1061 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Oct 19 11:30:16 2023 +0200
+++ b/src/HOL/Product_Type.thy	Thu Oct 19 16:31:17 2023 +0200
@@ -1303,9 +1303,8 @@
 
 ML_file \<open>Tools/set_comprehension_pointfree.ML\<close>
 
-simproc_setup set_comprehension ("Collect P") =
+simproc_setup passive 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>
 
diff -r 200daaab2578 -r 807b249f1061 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Oct 19 11:30:16 2023 +0200
+++ b/src/HOL/Tools/record.ML	Thu Oct 19 16:31:17 2023 +0200
@@ -1117,8 +1117,8 @@
 
 val simproc =
   Simplifier.simproc_setup
-   {name = \<^binding>\<open>select_update\<close>, lhss = ["x::'a::{}"], proc = K select_update_proc,
-     passive = false};
+   {passive = false, name = \<^binding>\<open>select_update\<close>, lhss = ["x::'a::{}"],
+     proc = K select_update_proc};
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
@@ -1285,7 +1285,7 @@
 
 val upd_simproc =
   Simplifier.simproc_setup
-    {name = \<^binding>\<open>update\<close>, lhss = ["x::'a::{}"], proc = K upd_proc, passive = false};
+    {passive = false, name = \<^binding>\<open>update\<close>, lhss = ["x::'a::{}"], proc = K upd_proc};
 
 end;
 
@@ -1318,7 +1318,7 @@
 
 val eq_simproc =
   Simplifier.simproc_setup
-    {name = \<^binding>\<open>eq\<close>, lhss = ["r = s"], proc = K eq_proc, passive = false};
+    {passive = false, name = \<^binding>\<open>eq\<close>, lhss = ["r = s"], proc = K eq_proc};
 
 
 (* split_simproc *)
@@ -1397,7 +1397,7 @@
 
 val ex_sel_eq_simproc =
   Simplifier.simproc_setup
-    {name = \<^binding>\<open>ex_sel_eq\<close>, lhss = ["Ex t"], proc = K ex_sel_eq_proc, passive = true};
+    {passive = true, name = \<^binding>\<open>ex_sel_eq\<close>, lhss = ["Ex t"], proc = K ex_sel_eq_proc};
 
 
 (* split_simp_tac *)
diff -r 200daaab2578 -r 807b249f1061 src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Thu Oct 19 11:30:16 2023 +0200
+++ b/src/Pure/ex/Def.thy	Thu Oct 19 16:31:17 2023 +0200
@@ -67,7 +67,7 @@
 
 val _ =
   Simplifier.simproc_setup
-    {name = \<^binding>\<open>expand_def\<close>, lhss = ["x::'a"], passive = false, proc = K get_def};
+    {passive = false, name = \<^binding>\<open>expand_def\<close>, lhss = ["x::'a"], proc = K get_def};
 
 
 (* Isar command *)
diff -r 200daaab2578 -r 807b249f1061 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Oct 19 11:30:16 2023 +0200
+++ b/src/Pure/simplifier.ML	Thu Oct 19 16:31:17 2023 +0200
@@ -40,10 +40,10 @@
   val make_simproc: Proof.context -> string ->
     {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
   type 'a simproc_spec =
-    {lhss: 'a list, passive: bool, proc: morphism -> Proof.context -> cterm -> thm option}
+    {passive: bool, lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
   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
-  type 'a simproc_setup = {name: binding, lhss: string list, passive: bool, proc: 'a}
+  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 -> Proof.context -> cterm -> thm option) simproc_setup
   val simproc_setup_parser: Input.source simproc_setup parser
@@ -138,13 +138,13 @@
   end;
 
 type 'a simproc_spec =
- {lhss: 'a list,
-  passive: bool,
+ {passive: bool,
+  lhss: 'a list,
   proc: morphism -> Proof.context -> cterm -> thm option};
 
 local
 
-fun def_simproc prep b {lhss, passive, proc} lthy =
+fun def_simproc prep b {passive, lhss, proc} lthy =
   let
     val simproc0 =
       make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
@@ -172,21 +172,22 @@
 
 (* implicit simproc_setup *)
 
-type 'a simproc_setup = {name: binding, lhss: string list, passive: bool, proc: 'a};
+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 -> Proof.context -> cterm -> thm option) simproc_setup;
 
 val simproc_setup_parser : simproc_setup_input parser =
-  Parse.binding -- (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") --
-    (Parse.$$$ "=" |-- Parse.ML_source) -- Parse.opt_keyword "passive"
-  >> (fn (((name, lhss), proc), passive) =>
-        {name = name, lhss = lhss, passive = passive, proc = proc});
+  Scan.optional (Parse.$$$ "passive" >> K true) false --
+  Parse.binding --
+    (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") --
+    (Parse.$$$ "=" |-- Parse.ML_source)
+  >> (fn (((a, b), c), d) => {passive = a, name = b, lhss = c, proc = d});
 
-fun simproc_setup_ml ({name, lhss, passive, proc}: simproc_setup_input) =
+fun simproc_setup_ml ({name, passive, lhss, proc}: simproc_setup_input) =
   ML_Lex.read
-    ("{name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
+    ("{passive = " ^ Bool.toString passive ^
+     ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
      ", lhss = " ^ ML_Syntax.print_strings lhss ^
-     ", passive = " ^ Bool.toString passive ^
      ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}";
 
 fun simproc_setup ({name, lhss, passive, proc}: simproc_setup_internal) =