src/HOL/Tools/inductive.ML

   val params_of: thm -> term list
   val partition_rules: thm -> thm list -> (string * thm list) list
   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 =
 sig
   include BASIC_INDUCTIVE

 
 val mono_del =
   Thm.declaration_attribute (fn thm => fn context =>
     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 *)
 
 val get_equations = #equations o rep_data;

   in lthy |> Local_Theory.notes facts end;
 
 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 *)
 
 fun mk_simp_eq ctxt prop =

     map (mtch o apsnd prop_of) (cases ~~ intros)
   end;
 
 
 
-(** 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 --
   Scan.optional Parse_Spec.where_alt_specs [] --
   Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) []