# HG changeset patch
# User wenzelm
# Date 1414605709 -3600
# Node ID 2ed2eaabe3dfff4ad75139e59f19f62ab9890866
# Parent  2065f49da190d694868e13ba64d606294fd2e5ad
modernized setup;

diff -r 2065f49da190 -r 2ed2eaabe3df src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/FOL/FOL.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -12,8 +12,6 @@
 ML_file "~~/src/Provers/classical.ML"
 ML_file "~~/src/Provers/blast.ML"
 ML_file "~~/src/Provers/clasimp.ML"
-ML_file "~~/src/Tools/induct.ML"
-ML_file "~~/src/Tools/case_product.ML"
 
 
 subsection {* The classical axiom *}
@@ -181,8 +179,6 @@
 open Basic_Classical;
 *}
 
-setup Cla.setup
-
 (*Propositional rules*)
 lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
   and [elim!] = conjE disjE impCE FalseE iffCE
@@ -209,8 +205,6 @@
   val blast_tac = Blast.blast_tac;
 *}
 
-setup Blast.setup
-
 
 lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
   by blast
@@ -344,14 +338,12 @@
   |> simpset_of;
 *}
 
-setup {* map_theory_simpset (put_simpset FOL_ss) *}
-
-setup "Simplifier.method_setup Splitter.split_modifiers"
-setup Splitter.setup
-setup clasimp_setup
+setup {*
+  map_theory_simpset (put_simpset FOL_ss) #>
+  Simplifier.method_setup Splitter.split_modifiers
+*}
 
 ML_file "~~/src/Tools/eqsubst.ML"
-setup EqSubst.setup
 
 
 subsection {* Other simple lemmas *}
@@ -418,6 +410,7 @@
 
 text {* Method setup. *}
 
+ML_file "~~/src/Tools/induct.ML"
 ML {*
   structure Induct = Induct
   (
@@ -431,10 +424,9 @@
   );
 *}
 
-setup Induct.setup
 declare case_split [cases type: o]
 
-setup Case_Product.setup
+ML_file "~~/src/Tools/case_product.ML"
 
 
 hide_const (open) eq
diff -r 2065f49da190 -r 2ed2eaabe3df src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/FOL/IFOL.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -591,7 +591,6 @@
 open Hypsubst;
 *}
 
-setup hypsubst_setup
 ML_file "intprover.ML"
 
 
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/BNF_Greatest_Fixpoint.thy
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -17,9 +17,7 @@
   "primcorec" :: thy_decl
 begin
 
-setup {*
-Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
-*}
+setup {* Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj} *}
 
 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by simp
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Fields.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -23,8 +23,7 @@
   fixes inverse :: "'a \<Rightarrow> 'a"
     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
 
-setup {* Sign.add_const_constraint
-  (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
 
 
 context semiring
@@ -47,8 +46,7 @@
 
 end
 
-setup {* Sign.add_const_constraint
-  (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
 
 text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
 
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Fun_Def.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -106,11 +106,6 @@
   Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac)
 *} "prove an induction principle"
 
-setup {*
-  Function.setup
-  #> Function_Fun.setup
-*}
-
 
 subsection {* Measure functions *}
 
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/HOL.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -27,18 +27,12 @@
 ML_file "~~/src/Tools/eqsubst.ML"
 ML_file "~~/src/Provers/quantifier1.ML"
 ML_file "~~/src/Tools/atomize_elim.ML"
-ML_file "~~/src/Tools/induct.ML"
 ML_file "~~/src/Tools/cong_tac.ML"
-ML_file "~~/src/Tools/intuitionistic.ML"
+ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
 ML_file "~~/src/Tools/project_rule.ML"
 ML_file "~~/src/Tools/subtyping.ML"
 ML_file "~~/src/Tools/case_product.ML"
 
-setup {*
-  Intuitionistic.method_setup @{binding iprover}
-  #> Subtyping.setup
-  #> Case_Product.setup
-*}
 
 ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
 
@@ -231,7 +225,7 @@
 lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t"
   by (rule trans [OF _ sym])
 
-lemma meta_eq_to_obj_eq: 
+lemma meta_eq_to_obj_eq:
   assumes meq: "A == B"
   shows "A = B"
   by (unfold meq) (rule refl)
@@ -847,26 +841,23 @@
   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
 );
 
-structure Basic_Classical: BASIC_CLASSICAL = Classical; 
+structure Basic_Classical: BASIC_CLASSICAL = Classical;
 open Basic_Classical;
 *}
 
-setup Classical.setup
-
 setup {*
-let
-  fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
-    | non_bool_eq _ = false;
-  fun hyp_subst_tac' ctxt =
-    SUBGOAL (fn (goal, i) =>
-      if Term.exists_Const non_bool_eq goal
-      then Hypsubst.hyp_subst_tac ctxt i
-      else no_tac);
-in
-  Hypsubst.hypsubst_setup
   (*prevent substitution on bool*)
-  #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
-end
+  let
+    fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
+      | non_bool_eq _ = false;
+    fun hyp_subst_tac' ctxt =
+      SUBGOAL (fn (goal, i) =>
+        if Term.exists_Const non_bool_eq goal
+        then Hypsubst.hyp_subst_tac ctxt i
+        else no_tac);
+  in
+    Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
+  end
 *}
 
 declare iffI [intro!]
@@ -932,8 +923,6 @@
   val blast_tac = Blast.blast_tac;
 *}
 
-setup Blast.setup
-
 
 subsubsection {* Simplifier *}
 
@@ -1197,18 +1186,14 @@
 ML_file "Tools/simpdata.ML"
 ML {* open Simpdata *}
 
-setup {* map_theory_simpset (put_simpset HOL_basic_ss) *}
+setup {*
+  map_theory_simpset (put_simpset HOL_basic_ss) #>
+  Simplifier.method_setup Splitter.split_modifiers
+*}
 
 simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
 simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
 
-setup {*
-  Simplifier.method_setup Splitter.split_modifiers
-  #> Splitter.setup
-  #> clasimp_setup
-  #> EqSubst.setup
-*}
-
 text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *}
 
 simproc_setup neq ("x = y") = {* fn _ =>
@@ -1467,6 +1452,7 @@
 
 text {* Method setup. *}
 
+ML_file "~~/src/Tools/induct.ML"
 ML {*
 structure Induct = Induct
 (
@@ -1484,7 +1470,6 @@
 ML_file "~~/src/Tools/induction.ML"
 
 setup {*
-  Induct.setup #> Induction.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
     addsimprocs
       [Simplifier.simproc_global @{theory} "swap_induct_false"
@@ -1558,13 +1543,12 @@
 lemma [induct_simp]: "induct_implies induct_true P == P"
   by (simp add: induct_implies_def induct_true_def)
 
-lemma [induct_simp]: "(x = x) = True" 
+lemma [induct_simp]: "(x = x) = True"
   by (rule simp_thms)
 
 hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
 
 ML_file "~~/src/Tools/induct_tacs.ML"
-setup Induct_Tacs.setup
 
 
 subsubsection {* Coherent logic *}
@@ -1640,8 +1624,8 @@
 lemmas eq_sym_conv = eq_commute
 
 lemma nnf_simps:
-  "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)" 
-  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))" 
+  "(\<not>(P \<and> Q)) = (\<not> P \<or> \<not> Q)" "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
+  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
   "(\<not> \<not>(P)) = P"
 by blast+
 
@@ -1737,10 +1721,11 @@
   by (fact arg_cong)
 
 setup {*
-  Code_Preproc.map_pre (put_simpset HOL_basic_ss)
-  #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
-  #> Code_Simp.map_ss (put_simpset HOL_basic_ss
-    #> Simplifier.add_cong @{thm conj_left_cong} #> Simplifier.add_cong @{thm disj_left_cong})
+  Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
+  Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
+  Code_Simp.map_ss (put_simpset HOL_basic_ss #>
+  Simplifier.add_cong @{thm conj_left_cong} #>
+  Simplifier.add_cong @{thm disj_left_cong})
 *}
 
 
@@ -1799,7 +1784,7 @@
 text {* More about @{typ prop} *}
 
 lemma [code nbe]:
-  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
+  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
     and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
     and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
 
@@ -1828,9 +1813,7 @@
   "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   by (simp add: equal)
 
-setup {*
-  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
-*}
+setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"}) *}
 
 lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
 proof
@@ -1843,14 +1826,10 @@
   show "PROP ?ofclass" proof
   qed (simp add: `PROP ?equal`)
 qed
-  
-setup {*
-  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
-*}
 
-setup {*
-  Nbe.add_const_alias @{thm equal_alias_cert}
-*}
+setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"}) *}
+
+setup {* Nbe.add_const_alias @{thm equal_alias_cert} *}
 
 text {* Cases *}
 
@@ -1860,8 +1839,8 @@
   using assms by simp_all
 
 setup {*
-  Code.add_case @{thm Let_case_cert}
-  #> Code.add_undefined @{const_name undefined}
+  Code.add_case @{thm Let_case_cert} #>
+  Code.add_undefined @{const_name undefined}
 *}
 
 declare [[code abort: undefined]]
@@ -1877,7 +1856,7 @@
 | constant True \<rightharpoonup>
     (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
 | constant False \<rightharpoonup>
-    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" 
+    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
 
 code_reserved SML
   bool true false
@@ -1936,13 +1915,13 @@
 subsubsection {* Evaluation and normalization by evaluation *}
 
 method_setup eval = {*
-let
-  fun eval_tac ctxt =
-    let val conv = Code_Runtime.dynamic_holds_conv ctxt
-    in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
-in
-  Scan.succeed (SIMPLE_METHOD' o eval_tac)
-end
+  let
+    fun eval_tac ctxt =
+      let val conv = Code_Runtime.dynamic_holds_conv ctxt
+      in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
+  in
+    Scan.succeed (SIMPLE_METHOD' o eval_tac)
+  end
 *} "solve goal by evaluation"
 
 method_setup normalization = {*
@@ -1989,23 +1968,23 @@
 subsection {* Legacy tactics and ML bindings *}
 
 ML {*
-(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
-local
-  fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
-    | wrong_prem (Bound _) = true
-    | wrong_prem _ = false;
-  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
-in
-  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
-  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
-end;
+  (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
+  local
+    fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
+      | wrong_prem (Bound _) = true
+      | wrong_prem _ = false;
+    val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+  in
+    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
+    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
+  end;
 
-local
-  val nnf_ss =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
-in
-  fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
-end
+  local
+    val nnf_ss =
+      simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
+  in
+    fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
+  end
 *}
 
 hide_const (open) eq equal
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Orderings.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -400,6 +400,8 @@
 sig
   val print_structures: Proof.context -> unit
   val order_tac: Proof.context -> thm list -> int -> tactic
+  val add_struct: string * term list -> string -> attribute
+  val del_struct: string * term list -> attribute
 end;
 
 structure Orders: ORDERS =
@@ -483,26 +485,24 @@
 
 (* attributes *)
 
-fun add_struct_thm s tag =
+fun add_struct s tag =
   Thm.declaration_attribute
     (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
 fun del_struct s =
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
 
-val _ =
-  Theory.setup
-    (Attrib.setup @{binding order}
-      (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
-        Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
-        Scan.repeat Args.term
-        >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
-             | ((NONE, n), ts) => del_struct (n, ts)))
-      "theorems controlling transitivity reasoner");
-
 end;
 *}
 
+attribute_setup order = {*
+  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
+    Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
+    Scan.repeat Args.term
+    >> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag
+         | ((NONE, n), ts) => Orders.del_struct (n, ts))
+*} "theorems controlling transitivity reasoner"
+
 method_setup order = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
 *} "transitivity reasoner"
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Product_Type.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -50,9 +50,7 @@
   shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
   using assms by simp_all
 
-setup {*
-  Code.add_case @{thm If_case_cert}
-*}
+setup {* Code.add_case @{thm If_case_cert} *}
 
 code_printing
   constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -618,8 +618,6 @@
 
 ML_file "Tools/Quickcheck/exhaustive_generators.ML"
 
-setup Exhaustive_Generators.setup
-
 declare [[quickcheck_batch_tester = exhaustive]]
 
 subsection {* Defining generators for abstract types *}
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -197,8 +197,6 @@
 
 ML_file "Tools/Quickcheck/narrowing_generators.ML"
 
-setup Narrowing_Generators.setup
-
 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
 where
   "narrowing_dummy_partial_term_of = partial_term_of"
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -207,7 +207,6 @@
 
 ML_file "Tools/Quickcheck/quickcheck_common.ML" 
 ML_file "Tools/Quickcheck/random_generators.ML"
-setup Random_Generators.setup
 
 
 subsection {* Code setup *}
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Wed Oct 29 19:01:49 2014 +0100
@@ -8,8 +8,6 @@
 imports Numeral_Simprocs Nat_Transfer
 begin
 
-ML_file "Tools/semiring_normalizer.ML"
-
 text {* Prelude *}
 
 class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
@@ -69,7 +67,7 @@
 
 text {* Semiring normalization proper *}
 
-setup Semiring_Normalizer.setup
+ML_file "Tools/semiring_normalizer.ML"
 
 context comm_semiring_1
 begin
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -14,8 +14,6 @@
   val add_fun_cmd : (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> Function_Common.function_config ->
     bool -> local_theory -> Proof.context
-
-  val setup : theory -> theory
 end
 
 structure Function_Fun : FUNCTION_FUN =
@@ -148,8 +146,8 @@
   else
     Function_Common.empty_preproc check_defs config ctxt fixes spec
 
-val setup =
-  Context.theory_map (Function_Common.set_preproc sequential_preproc)
+val _ = Theory.setup (Context.theory_map (Function_Common.set_preproc sequential_preproc))
+
 
 
 val fun_config = FunctionConfig { sequential=true, default=NONE,
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -32,7 +32,6 @@
   val termination : term option -> local_theory -> Proof.state
   val termination_cmd : string option -> local_theory -> Proof.state
 
-  val setup : theory -> theory
   val get_congs : Proof.context -> thm list
 
   val get_info : Proof.context -> term -> info
@@ -264,7 +263,6 @@
 
 (* Datatype hook to declare datatype congs as "function_congs" *)
 
-
 fun add_case_cong n thy =
   let
     val cong = #case_cong (Old_Datatype_Data.the_info thy n)
@@ -274,12 +272,10 @@
       (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
   end
 
-val setup_case_cong = Old_Datatype_Data.interpretation (K (fold add_case_cong))
+val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
 
 
-(* setup *)
-
-val setup = setup_case_cong
+(* get info *)
 
 val get_congs = Function_Context_Tree.get_function_congs
 
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -21,7 +21,6 @@
   val quickcheck_pretty : bool Config.T
   val setup_exhaustive_datatype_interpretation : theory -> theory
   val setup_bounded_forall_datatype_interpretation : theory -> theory
-  val setup: theory -> theory
   
   val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
     (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
@@ -547,11 +546,12 @@
 
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
-val setup =
-  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
-    (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
-  #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
-  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
-  #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
+val _ =
+  Theory.setup
+   (Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
+      (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
+    #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
+    #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
+    #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)));
 
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -16,7 +16,6 @@
     | Empty_Assignment
   val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
   val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
-  val setup: theory -> theory
 end;
 
 structure Narrowing_Generators : NARROWING_GENERATORS =
@@ -522,11 +521,12 @@
 
 val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
 
-val setup =
-  Code.datatype_interpretation ensure_partial_term_of
-  #> Code.datatype_interpretation ensure_partial_term_of_code
-  #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
-    (@{sort narrowing}, instantiate_narrowing_datatype)
-  #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
+val _ =
+  Theory.setup
+   (Code.datatype_interpretation ensure_partial_term_of
+    #> Code.datatype_interpretation ensure_partial_term_of_code
+    #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
+      (@{sort narrowing}, instantiate_narrowing_datatype)
+    #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))));
     
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -18,7 +18,6 @@
     -> Proof.context -> Proof.context
   val instantiate_random_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
     (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
-  val setup: theory -> theory
 end;
 
 structure Random_Generators : RANDOM_GENERATORS =
@@ -469,9 +468,10 @@
 
 val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
 
-val setup =
-  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
-    (@{sort random}, instantiate_random_datatype)
-  #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
+val _ =
+  Theory.setup
+   (Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
+      (@{sort random}, instantiate_random_datatype) #>
+    Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals))));
 
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -41,8 +41,6 @@
        main: Proof.context -> conv,
        pow: Proof.context -> conv,
        sub: Proof.context -> conv}
-
-  val setup: theory -> theory
 end
 
 structure Semiring_Normalizer: SEMIRING_NORMALIZER = 
@@ -912,20 +910,21 @@
 
 in
 
-val setup =
-  Attrib.setup @{binding normalizer}
-    (Scan.lift (Args.$$$ delN >> K del) ||
-      ((keyword2 semiringN opsN |-- terms) --
-       (keyword2 semiringN rulesN |-- thms)) --
-      (optional (keyword2 ringN opsN |-- terms) --
-       optional (keyword2 ringN rulesN |-- thms)) --
-      (optional (keyword2 fieldN opsN |-- terms) --
-       optional (keyword2 fieldN rulesN |-- thms)) --
-      optional (keyword2 idomN rulesN |-- thms) --
-      optional (keyword2 idealN rulesN |-- thms)
-      >> (fn ((((sr, r), f), id), idl) => 
-             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
-    "semiring normalizer data";
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding normalizer}
+      (Scan.lift (Args.$$$ delN >> K del) ||
+        ((keyword2 semiringN opsN |-- terms) --
+         (keyword2 semiringN rulesN |-- thms)) --
+        (optional (keyword2 ringN opsN |-- terms) --
+         optional (keyword2 ringN rulesN |-- thms)) --
+        (optional (keyword2 fieldN opsN |-- terms) --
+         optional (keyword2 fieldN rulesN |-- thms)) --
+        optional (keyword2 idomN rulesN |-- thms) --
+        optional (keyword2 idealN rulesN |-- thms)
+        >> (fn ((((sr, r), f), id), idl) => 
+               add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
+      "semiring normalizer data");
 
 end;
 
diff -r 2065f49da190 -r 2ed2eaabe3df src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/blast.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -62,7 +62,6 @@
   val trace: bool Config.T
   val stats: bool Config.T
   val blast_tac: Proof.context -> int -> tactic
-  val setup: theory -> theory
   (*debugging tools*)
   type branch
   val tryIt: Proof.context -> int -> string ->
@@ -77,7 +76,7 @@
 
 (* options *)
 
-val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
+val depth_limit = Attrib.setup_config_int @{binding blast_depth_limit} (K 20);
 val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
 val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
 
@@ -1294,14 +1293,15 @@
   in {fullTrace = !fullTrace, result = res} end;
 
 
+
 (** method setup **)
 
-val setup =
-  setup_depth_limit #>
-  Method.setup @{binding blast}
-    (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
-      (fn NONE => SIMPLE_METHOD' o blast_tac
-        | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
-    "classical tableau prover";
+val _ =
+  Theory.setup
+    (Method.setup @{binding blast}
+      (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
+        (fn NONE => SIMPLE_METHOD' o blast_tac
+          | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
+      "classical tableau prover");
 
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/clasimp.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -31,7 +31,6 @@
   val iff_del: attribute
   val iff_modifiers: Method.modifier parser list
   val clasimp_modifiers: Method.modifier parser list
-  val clasimp_setup: theory -> theory
 end;
 
 functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
@@ -180,10 +179,14 @@
 
 (* attributes *)
 
-fun iff_att x = (Scan.lift
- (Args.del >> K iff_del ||
-  Scan.option Args.add -- Args.query >> K iff_add' ||
-  Scan.option Args.add >> K iff_add)) x;
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding iff}
+      (Scan.lift
+        (Args.del >> K iff_del ||
+          Scan.option Args.add -- Args.query >> K iff_add' ||
+          Scan.option Args.add >> K iff_add))
+      "declaration of Simplifier / Classical rules");
 
 
 (* method modifiers *)
@@ -211,17 +214,14 @@
   (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
     | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
 
-
-(* theory setup *)
-
-val clasimp_setup =
-  Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
-  Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
-  Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
-  Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
-  Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
-  Method.setup @{binding auto} auto_method "auto" #>
-  Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
-    "clarify simplified goal";
+val _ =
+  Theory.setup
+   (Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
+    Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
+    Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
+    Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
+    Method.setup @{binding auto} auto_method "auto" #>
+    Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
+      "clarify simplified goal");
 
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/classical.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -124,7 +124,6 @@
     (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
   val cla_method':
     (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
-  val setup: theory -> theory
 end;
 
 
@@ -882,17 +881,18 @@
 val elimN = "elim";
 val destN = "dest";
 
-val setup_attrs =
-  Attrib.setup @{binding swapped} (Scan.succeed swapped)
-    "classical swap of introduction rule" #>
-  Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
-    "declaration of Classical destruction rule" #>
-  Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
-    "declaration of Classical elimination rule" #>
-  Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
-    "declaration of Classical introduction rule" #>
-  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
-    "remove declaration of intro/elim/dest rule";
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding swapped} (Scan.succeed swapped)
+      "classical swap of introduction rule" #>
+    Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
+      "declaration of Classical destruction rule" #>
+    Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
+      "declaration of Classical elimination rule" #>
+    Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
+      "declaration of Classical introduction rule" #>
+    Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+      "remove declaration of intro/elim/dest rule");
 
 
 
@@ -941,46 +941,40 @@
 
 
 
-(** setup_methods **)
+(** method setup **)
 
-val setup_methods =
-  Method.setup @{binding default}
-   (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
-    "apply some intro/elim rule (potentially classical)" #>
-  Method.setup @{binding rule}
-    (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
-    "apply some intro/elim rule (potentially classical)" #>
-  Method.setup @{binding contradiction}
-    (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
-    "proof by contradiction" #>
-  Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
-    "repeatedly apply safe steps" #>
-  Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
-  Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
-  Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
-  Method.setup @{binding deepen}
-    (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
-      >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
-    "classical prover (iterative deepening)" #>
-  Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
-    "classical prover (apply safe rules)" #>
-  Method.setup @{binding safe_step} (cla_method' safe_step_tac)
-    "single classical step (safe rules)" #>
-  Method.setup @{binding inst_step} (cla_method' inst_step_tac)
-    "single classical step (safe rules, allow instantiations)" #>
-  Method.setup @{binding step} (cla_method' step_tac)
-    "single classical step (safe and unsafe rules)" #>
-  Method.setup @{binding slow_step} (cla_method' slow_step_tac)
-    "single classical step (safe and unsafe rules, allow backtracking)" #>
-  Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
-    "single classical step (safe rules, without splitting)";
-
-
-
-(** theory setup **)
-
-val setup = setup_attrs #> setup_methods;
-
+val _ =
+  Theory.setup
+   (Method.setup @{binding default}
+     (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
+      "apply some intro/elim rule (potentially classical)" #>
+    Method.setup @{binding rule}
+      (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
+      "apply some intro/elim rule (potentially classical)" #>
+    Method.setup @{binding contradiction}
+      (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
+      "proof by contradiction" #>
+    Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
+      "repeatedly apply safe steps" #>
+    Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
+    Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
+    Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
+    Method.setup @{binding deepen}
+      (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
+        >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
+      "classical prover (iterative deepening)" #>
+    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
+      "classical prover (apply safe rules)" #>
+    Method.setup @{binding safe_step} (cla_method' safe_step_tac)
+      "single classical step (safe rules)" #>
+    Method.setup @{binding inst_step} (cla_method' inst_step_tac)
+      "single classical step (safe rules, allow instantiations)" #>
+    Method.setup @{binding step} (cla_method' step_tac)
+      "single classical step (safe and unsafe rules)" #>
+    Method.setup @{binding slow_step} (cla_method' slow_step_tac)
+      "single classical step (safe and unsafe rules, allow backtracking)" #>
+    Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
+      "single classical step (safe rules, without splitting)");
 
 
 (** outer syntax **)
diff -r 2065f49da190 -r 2ed2eaabe3df src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/hypsubst.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -52,7 +52,6 @@
   val hyp_subst_tac          : Proof.context -> int -> tactic
   val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
-  val hypsubst_setup         : theory -> theory
 end;
 
 functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
@@ -120,7 +119,7 @@
                handle TERM _ => eq_var_aux (k+1) B (A :: hs)
                  | Match => eq_var_aux (k+1) B (A :: hs))
       | eq_var_aux k _ _ = raise EQ_VAR
-  
+
   in  eq_var_aux 0 t [] end;
 
 val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
@@ -228,11 +227,10 @@
     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
     if thin then thin_free_eq_tac else K no_tac];
 
-val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool
-    @{binding hypsubst_thin} (K false);
+val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
 
-fun hyp_subst_tac ctxt = hyp_subst_tac_thin
-    (Config.get ctxt hyp_subst_thin) ctxt
+fun hyp_subst_tac ctxt =
+  hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
 
 (*Substitutes for Bound variables only -- this is always safe*)
 fun bound_hyp_subst_tac ctxt =
@@ -296,18 +294,18 @@
   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
 
 
-(* theory setup *)
+(* method setup *)
 
-val hypsubst_setup =
-  Method.setup @{binding hypsubst}
-    (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
-    "substitution using an assumption (improper)" #>
-  Method.setup @{binding hypsubst_thin}
-    (Scan.succeed (fn ctxt => SIMPLE_METHOD'
-        (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
-    "substitution using an assumption, eliminating assumptions" #>
-  hyp_subst_thin_setup #>
-  Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
-    "simple substitution";
+val _ =
+  Theory.setup
+   (Method.setup @{binding hypsubst}
+      (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
+      "substitution using an assumption (improper)" #>
+    Method.setup @{binding hypsubst_thin}
+      (Scan.succeed (fn ctxt => SIMPLE_METHOD'
+          (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
+      "substitution using an assumption, eliminating assumptions" #>
+    Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
+      "simple substitution");
 
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Provers/splitter.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -37,7 +37,6 @@
   val split_add: attribute
   val split_del: attribute
   val split_modifiers : Method.modifier parser list
-  val setup: theory -> theory
 end;
 
 functor Splitter(Data: SPLITTER_DATA): SPLITTER =
@@ -453,6 +452,11 @@
 val split_add = Simplifier.attrib add_split;
 val split_del = Simplifier.attrib del_split;
 
+val _ =
+  Theory.setup
+    (Attrib.setup @{binding split}
+      (Attrib.add_del split_add split_del) "declare case split rule");
+
 
 (* methods *)
 
@@ -461,14 +465,10 @@
   Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
   Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
 
-
-(* theory setup *)
-
-val setup =
-  Attrib.setup @{binding split}
-    (Attrib.add_del split_add split_del) "declare case split rule" #>
-  Method.setup @{binding split}
-    (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
-    "apply case split rule";
+val _ =
+  Theory.setup
+    (Method.setup @{binding split}
+      (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
+      "apply case split rule");
 
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/Tools/case_product.ML
--- a/src/Tools/case_product.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/case_product.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -12,7 +12,7 @@
 sig
   val combine: Proof.context -> thm -> thm -> thm
   val combine_annotated: Proof.context -> thm -> thm -> thm
-  val setup: theory -> theory
+  val annotation: thm -> thm -> attribute
 end
 
 structure Case_Product: CASE_PRODUCT =
@@ -104,15 +104,15 @@
 
 (* attribute setup *)
 
-val case_prod_attr =
-  let
-    fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
-  in
-    Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
-      combine_list (Context.proof_of ctxt) thms thm))
-  end
-
-val setup =
-  Attrib.setup @{binding case_product} case_prod_attr "product with other case rules"
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding case_product}
+      let
+        fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
+      in
+        Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
+          combine_list (Context.proof_of ctxt) thms thm))
+      end
+    "product with other case rules")
 
 end
diff -r 2065f49da190 -r 2ed2eaabe3df src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/eqsubst.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -45,8 +45,6 @@
   val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
   val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
   val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
-
-  val setup : theory -> theory
 end;
 
 structure EqSubst: EQSUBST =
@@ -418,12 +416,12 @@
 (* combination method that takes a flag (true indicates that subst
    should be done to an assumption, false = apply to the conclusion of
    the goal) as well as the theorems to use *)
-val setup =
-  Method.setup @{binding subst}
-    (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
-        Attrib.thms >>
-      (fn ((asm, occs), inthms) => fn ctxt =>
-        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
-    "single-step substitution";
+val _ =
+  Theory.setup
+    (Method.setup @{binding subst}
+      (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+        Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt =>
+          SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
+      "single-step substitution");
 
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/induct.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -89,7 +89,6 @@
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic) ->
    theory -> theory
-  val setup: theory -> theory
 end;
 
 functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
@@ -368,15 +367,16 @@
 
 in
 
-val attrib_setup =
-  Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
-    "declaration of cases rule" #>
-  Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
-    "declaration of induction rule" #>
-  Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
-    "declaration of coinduction rule" #>
-  Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
-    "declaration of rules for simplifying induction or cases rules";
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
+      "declaration of cases rule" #>
+    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
+      "declaration of induction rule" #>
+    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
+      "declaration of coinduction rule" #>
+    Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
+      "declaration of rules for simplifying induction or cases rules");
 
 end;
 
@@ -923,14 +923,15 @@
 
 in
 
-val cases_setup =
-  Method.setup @{binding cases}
-    (Scan.lift (Args.mode no_simpN) --
-      (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
-      (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
-        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
-          (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
-    "case analysis on types or predicates/sets";
+val _ =
+  Theory.setup
+    (Method.setup @{binding cases}
+      (Scan.lift (Args.mode no_simpN) --
+        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
+        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
+          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
+            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
+      "case analysis on types or predicates/sets");
 
 fun gen_induct_setup binding tac =
   Method.setup binding
@@ -941,21 +942,16 @@
         Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
     "induction on types or predicates/sets";
 
-val induct_setup = gen_induct_setup @{binding induct} induct_tac;
+val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
 
-val coinduct_setup =
-  Method.setup @{binding coinduct}
-    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
-      (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
-        Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
-    "coinduction on types or predicates/sets";
+val _ =
+  Theory.setup
+    (Method.setup @{binding coinduct}
+      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
+        (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
+          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
+      "coinduction on types or predicates/sets");
 
 end;
 
-
-
-(** theory setup **)
-
-val setup = attrib_setup #> cases_setup  #> induct_setup #> coinduct_setup;
-
 end;
diff -r 2065f49da190 -r 2ed2eaabe3df src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/induct_tacs.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -10,7 +10,6 @@
   val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
   val induct_tac: Proof.context -> string option list list -> int -> tactic
   val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
-  val setup: theory -> theory
 end
 
 structure Induct_Tacs: INDUCT_TACS =
@@ -128,15 +127,16 @@
 
 in
 
-val setup =
-  Method.setup @{binding case_tac}
-    (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
-      (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
-    "unstructured case analysis on types" #>
-  Method.setup @{binding induct_tac}
-    (Args.goal_spec -- varss -- opt_rules >>
-      (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
-    "unstructured induction on types";
+val _ =
+  Theory.setup
+   (Method.setup @{binding case_tac}
+      (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
+        (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
+      "unstructured case analysis on types" #>
+    Method.setup @{binding induct_tac}
+      (Args.goal_spec -- varss -- opt_rules >>
+        (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
+      "unstructured induction on types");
 
 end;
 
diff -r 2065f49da190 -r 2ed2eaabe3df src/Tools/induction.ML
--- a/src/Tools/induction.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/induction.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -3,7 +3,6 @@
   val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
-  val setup: theory -> theory
 end
 
 structure Induction: INDUCTION =
@@ -37,7 +36,7 @@
 
 val induction_tac = Induct.gen_induct_tac (K name_hyps)
 
-val setup = Induct.gen_induct_setup @{binding induction} induction_tac
+val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
 
 end
 
diff -r 2065f49da190 -r 2ed2eaabe3df src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/Tools/subtyping.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -10,7 +10,6 @@
   val add_type_map: term -> Context.generic -> Context.generic
   val add_coercion: term -> Context.generic -> Context.generic
   val print_coercions: Proof.context -> unit
-  val setup: theory -> theory
 end;
 
 structure Subtyping: SUBTYPING =
@@ -884,9 +883,11 @@
 
 val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
 
-val add_term_check =
-  Syntax_Phases.term_check ~100 "coercions"
-    (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);
+val _ =
+  Theory.setup
+    (Context.theory_map
+      (Syntax_Phases.term_check ~100 "coercions"
+        (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt)));
 
 
 (* declarations *)
@@ -1088,26 +1089,26 @@
   end |> Pretty.writeln_chunks;
 
 
-(* theory setup *)
+(* attribute setup *)
 
 val parse_coerce_args =
   Args.$$$ "+" >> K PERMIT || Args.$$$ "-" >> K FORBID || Args.$$$ "0" >> K LEAVE
 
-val setup =
-  Context.theory_map add_term_check #>
-  Attrib.setup @{binding coercion}
-    (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
-    "declaration of new coercions" #>
-  Attrib.setup @{binding coercion_delete}
-    (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
-    "deletion of coercions" #>
-  Attrib.setup @{binding coercion_map}
-    (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
-    "declaration of new map functions" #>
-  Attrib.setup @{binding coercion_args}
-    (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
-      (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
-    "declaration of new constants with coercion-invariant arguments";
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding coercion}
+      (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
+      "declaration of new coercions" #>
+    Attrib.setup @{binding coercion_delete}
+      (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
+      "deletion of coercions" #>
+    Attrib.setup @{binding coercion_map}
+      (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
+      "declaration of new map functions" #>
+    Attrib.setup @{binding coercion_args}
+      (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
+        (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
+      "declaration of new constants with coercion-invariant arguments");
 
 
 (* outer syntax commands *)