modernized setup;

--- a/src/ZF/Inductive_ZF.thy	Wed Oct 29 19:01:49 2014 +0100
+++ b/src/ZF/Inductive_ZF.thy	Wed Oct 29 19:13:19 2014 +0100
@@ -34,9 +34,6 @@
 ML_file "Tools/induct_tacs.ML"
 ML_file "Tools/primrec_package.ML"
 
-setup IndCases.setup
-setup DatatypeTactics.setup
-
 ML {*
 structure Lfp =
   struct

--- a/src/ZF/Tools/ind_cases.ML	Wed Oct 29 19:01:49 2014 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Wed Oct 29 19:13:19 2014 +0100
@@ -8,7 +8,6 @@
 sig
   val declare: string -> (Proof.context -> conv) -> theory -> theory
   val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
-  val setup: theory -> theory
 end;
 
 structure IndCases: IND_CASES =
@@ -52,23 +51,21 @@
         map (Thm.no_attributes o single o smart_cases ctxt) props));
   in thy |> Global_Theory.note_thmss "" facts |> snd end;
 
-
-(* ind_cases method *)
-
-val setup =
-  Method.setup @{binding "ind_cases"}
-    (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
-      (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
-    "dynamic case analysis on sets";
-
-
-(* outer syntax *)
-
 val _ =
   Outer_Syntax.command @{command_spec "inductive_cases"}
     "create simplified instances of elimination rules (improper)"
     (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
       >> (Toplevel.theory o inductive_cases));
 
+
+(* ind_cases method *)
+
+val _ =
+  Theory.setup
+    (Method.setup @{binding "ind_cases"}
+      (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
+        (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
+      "dynamic case analysis on sets");
+
 end;
 

--- a/src/ZF/Tools/induct_tacs.ML	Wed Oct 29 19:01:49 2014 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Oct 29 19:13:19 2014 +0100
@@ -14,7 +14,6 @@
   val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
   val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
     (Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
-  val setup: theory -> theory
 end;
 
 
@@ -175,15 +174,16 @@
 
 (* theory setup *)
 
-val setup =
-  Method.setup @{binding induct_tac}
-    (Args.goal_spec -- Scan.lift Args.name >>
-      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
-    "induct_tac emulation (dynamic instantiation!)" #>
-  Method.setup @{binding case_tac}
-   (Args.goal_spec -- Scan.lift Args.name >>
-      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
-    "datatype case_tac emulation (dynamic instantiation!)";
+val _ =
+  Theory.setup
+    (Method.setup @{binding induct_tac}
+      (Args.goal_spec -- Scan.lift Args.name >>
+        (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
+      "induct_tac emulation (dynamic instantiation!)" #>
+    Method.setup @{binding case_tac}
+     (Args.goal_spec -- Scan.lift Args.name >>
+        (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
+      "datatype case_tac emulation (dynamic instantiation!)");
 
 
 (* outer syntax *)

--- a/src/ZF/Tools/typechk.ML	Wed Oct 29 19:01:49 2014 +0100
+++ b/src/ZF/Tools/typechk.ML	Wed Oct 29 19:13:19 2014 +0100
@@ -13,7 +13,6 @@
   val typecheck_tac: Proof.context -> tactic
   val type_solver_tac: Proof.context -> thm list -> int -> tactic
   val type_solver: solver
-  val setup: theory -> theory
 end;
 
 structure TypeCheck: TYPE_CHECK =
@@ -109,28 +108,25 @@
   Simplifier.mk_solver "ZF typecheck" (fn ctxt =>
     type_solver_tac ctxt (Simplifier.prems_of ctxt));
 
+val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt setSolver type_solver));
+
 
 (* concrete syntax *)
 
-val typecheck_setup =
-  Method.setup @{binding typecheck}
-    (Method.sections
-      [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
-       Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
-      >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
-    "ZF type-checking";
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del)
+      "declaration of type-checking rule" #>
+    Method.setup @{binding typecheck}
+      (Method.sections
+        [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
+         Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
+        >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
+      "ZF type-checking");
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
     (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_tcset o Toplevel.context_of)));
 
-
-(* theory setup *)
-
-val setup =
-  Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
-  typecheck_setup #>
-  map_theory_simpset (fn ctxt => ctxt setSolver type_solver);
-
 end;

--- a/src/ZF/upair.thy	Wed Oct 29 19:01:49 2014 +0100
+++ b/src/ZF/upair.thy	Wed Oct 29 19:13:19 2014 +0100
@@ -17,7 +17,6 @@
 begin
 
 ML_file "Tools/typechk.ML"
-setup TypeCheck.setup
 
 lemma atomize_ball [symmetric, rulify]:
      "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"