# HG changeset patch
# User wenzelm
# Date 1414579314 -3600
# Node ID fd3f893a40ea07644dbbca40d6f577ab54f0b7e3
# Parent  4c0ad4162cb799dd32b70d4759aa8575f14284a4
modernized setup;

diff -r 4c0ad4162cb7 -r fd3f893a40ea src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Oct 29 11:33:29 2014 +0100
+++ b/src/HOL/Inductive.thy	Wed Oct 29 11:41:54 2014 +0100
@@ -258,7 +258,6 @@
   Collect_mono in_mono vimage_mono
 
 ML_file "Tools/inductive.ML"
-setup Inductive.setup
 
 theorems [mono] =
   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
diff -r 4c0ad4162cb7 -r fd3f893a40ea src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Oct 29 11:33:29 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Oct 29 11:41:54 2014 +0100
@@ -64,7 +64,6 @@
   val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
   val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
   val infer_intro_vars: thm -> int -> thm list -> term list list
-  val setup: theory -> theory
 end;
 
 signature INDUCTIVE =
@@ -276,6 +275,11 @@
     map_data (fn (infos, monos, equations) =>
       (infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
 
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
+      "declaration of monotonicity rule");
+
 
 (* equations *)
 
@@ -587,19 +591,19 @@
 val inductive_cases = gen_inductive_cases Attrib.check_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
 
-
-val ind_cases_setup =
-  Method.setup @{binding ind_cases}
-    (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
-      Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
-      (fn (raw_props, fixes) => fn ctxt =>
-        let
-          val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
-          val props = Syntax.read_props ctxt' raw_props;
-          val ctxt'' = fold Variable.declare_term props ctxt';
-          val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
-        in Method.erule ctxt 0 rules end))
-    "dynamic case analysis on predicates";
+val _ =
+  Theory.setup
+    (Method.setup @{binding ind_cases}
+      (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
+        Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
+        (fn (raw_props, fixes) => fn ctxt =>
+          let
+            val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
+            val props = Syntax.read_props ctxt' raw_props;
+            val ctxt'' = fold Variable.declare_term props ctxt';
+            val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
+          in Method.erule ctxt 0 rules end))
+      "dynamic case analysis on predicates");
 
 
 (* derivation of simplified equation *)
@@ -1142,17 +1146,7 @@
 
 
 
-(** package setup **)
-
-(* setup theory *)
-
-val setup =
-  ind_cases_setup #>
-  Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
-    "declaration of monotonicity rule";
-
-
-(* outer syntax *)
+(** outer syntax **)
 
 fun gen_ind_decl mk_def coind =
   Parse.fixes -- Parse.for_fixes --