modernized setup;
authorwenzelm
Wed Oct 29 19:01:49 2014 +0100 (2014-10-29)
changeset 588262ed2eaabe3df
parent 58825 2065f49da190
child 58827 ea3a00678b87
child 58828 6d076fdd933d
modernized setup;
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/Fields.thy
src/HOL/Fun_Def.thy
src/HOL/HOL.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/semiring_normalizer.ML
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Tools/case_product.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
src/Tools/induct_tacs.ML
src/Tools/induction.ML
src/Tools/subtyping.ML
     1.1 --- a/src/FOL/FOL.thy	Wed Oct 29 17:01:44 2014 +0100
     1.2 +++ b/src/FOL/FOL.thy	Wed Oct 29 19:01:49 2014 +0100
     1.3 @@ -12,8 +12,6 @@
     1.4  ML_file "~~/src/Provers/classical.ML"
     1.5  ML_file "~~/src/Provers/blast.ML"
     1.6  ML_file "~~/src/Provers/clasimp.ML"
     1.7 -ML_file "~~/src/Tools/induct.ML"
     1.8 -ML_file "~~/src/Tools/case_product.ML"
     1.9  
    1.10  
    1.11  subsection {* The classical axiom *}
    1.12 @@ -181,8 +179,6 @@
    1.13  open Basic_Classical;
    1.14  *}
    1.15  
    1.16 -setup Cla.setup
    1.17 -
    1.18  (*Propositional rules*)
    1.19  lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
    1.20    and [elim!] = conjE disjE impCE FalseE iffCE
    1.21 @@ -209,8 +205,6 @@
    1.22    val blast_tac = Blast.blast_tac;
    1.23  *}
    1.24  
    1.25 -setup Blast.setup
    1.26 -
    1.27  
    1.28  lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    1.29    by blast
    1.30 @@ -344,14 +338,12 @@
    1.31    |> simpset_of;
    1.32  *}
    1.33  
    1.34 -setup {* map_theory_simpset (put_simpset FOL_ss) *}
    1.35 -
    1.36 -setup "Simplifier.method_setup Splitter.split_modifiers"
    1.37 -setup Splitter.setup
    1.38 -setup clasimp_setup
    1.39 +setup {*
    1.40 +  map_theory_simpset (put_simpset FOL_ss) #>
    1.41 +  Simplifier.method_setup Splitter.split_modifiers
    1.42 +*}
    1.43  
    1.44  ML_file "~~/src/Tools/eqsubst.ML"
    1.45 -setup EqSubst.setup
    1.46  
    1.47  
    1.48  subsection {* Other simple lemmas *}
    1.49 @@ -418,6 +410,7 @@
    1.50  
    1.51  text {* Method setup. *}
    1.52  
    1.53 +ML_file "~~/src/Tools/induct.ML"
    1.54  ML {*
    1.55    structure Induct = Induct
    1.56    (
    1.57 @@ -431,10 +424,9 @@
    1.58    );
    1.59  *}
    1.60  
    1.61 -setup Induct.setup
    1.62  declare case_split [cases type: o]
    1.63  
    1.64 -setup Case_Product.setup
    1.65 +ML_file "~~/src/Tools/case_product.ML"
    1.66  
    1.67  
    1.68  hide_const (open) eq
     2.1 --- a/src/FOL/IFOL.thy	Wed Oct 29 17:01:44 2014 +0100
     2.2 +++ b/src/FOL/IFOL.thy	Wed Oct 29 19:01:49 2014 +0100
     2.3 @@ -591,7 +591,6 @@
     2.4  open Hypsubst;
     2.5  *}
     2.6  
     2.7 -setup hypsubst_setup
     2.8  ML_file "intprover.ML"
     2.9  
    2.10  
     3.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 29 17:01:44 2014 +0100
     3.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 29 19:01:49 2014 +0100
     3.3 @@ -17,9 +17,7 @@
     3.4    "primcorec" :: thy_decl
     3.5  begin
     3.6  
     3.7 -setup {*
     3.8 -Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
     3.9 -*}
    3.10 +setup {* Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj} *}
    3.11  
    3.12  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    3.13    by simp
     4.1 --- a/src/HOL/Fields.thy	Wed Oct 29 17:01:44 2014 +0100
     4.2 +++ b/src/HOL/Fields.thy	Wed Oct 29 19:01:49 2014 +0100
     4.3 @@ -23,8 +23,7 @@
     4.4    fixes inverse :: "'a \<Rightarrow> 'a"
     4.5      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
     4.6  
     4.7 -setup {* Sign.add_const_constraint
     4.8 -  (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
     4.9 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    4.10  
    4.11  
    4.12  context semiring
    4.13 @@ -47,8 +46,7 @@
    4.14  
    4.15  end
    4.16  
    4.17 -setup {* Sign.add_const_constraint
    4.18 -  (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    4.19 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    4.20  
    4.21  text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
    4.22  
     5.1 --- a/src/HOL/Fun_Def.thy	Wed Oct 29 17:01:44 2014 +0100
     5.2 +++ b/src/HOL/Fun_Def.thy	Wed Oct 29 19:01:49 2014 +0100
     5.3 @@ -106,11 +106,6 @@
     5.4    Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac)
     5.5  *} "prove an induction principle"
     5.6  
     5.7 -setup {*
     5.8 -  Function.setup
     5.9 -  #> Function_Fun.setup
    5.10 -*}
    5.11 -
    5.12  
    5.13  subsection {* Measure functions *}
    5.14  
     6.1 --- a/src/HOL/HOL.thy	Wed Oct 29 17:01:44 2014 +0100
     6.2 +++ b/src/HOL/HOL.thy	Wed Oct 29 19:01:49 2014 +0100
     6.3 @@ -27,18 +27,12 @@
     6.4  ML_file "~~/src/Tools/eqsubst.ML"
     6.5  ML_file "~~/src/Provers/quantifier1.ML"
     6.6  ML_file "~~/src/Tools/atomize_elim.ML"
     6.7 -ML_file "~~/src/Tools/induct.ML"
     6.8  ML_file "~~/src/Tools/cong_tac.ML"
     6.9 -ML_file "~~/src/Tools/intuitionistic.ML"
    6.10 +ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
    6.11  ML_file "~~/src/Tools/project_rule.ML"
    6.12  ML_file "~~/src/Tools/subtyping.ML"
    6.13  ML_file "~~/src/Tools/case_product.ML"
    6.14  
    6.15 -setup {*
    6.16 -  Intuitionistic.method_setup @{binding iprover}
    6.17 -  #> Subtyping.setup
    6.18 -  #> Case_Product.setup
    6.19 -*}
    6.20  
    6.21  ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
    6.22  
    6.23 @@ -231,7 +225,7 @@
    6.24  lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t"
    6.25    by (rule trans [OF _ sym])
    6.26  
    6.27 -lemma meta_eq_to_obj_eq: 
    6.28 +lemma meta_eq_to_obj_eq:
    6.29    assumes meq: "A == B"
    6.30    shows "A = B"
    6.31    by (unfold meq) (rule refl)
    6.32 @@ -847,26 +841,23 @@
    6.33    val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
    6.34  );
    6.35  
    6.36 -structure Basic_Classical: BASIC_CLASSICAL = Classical; 
    6.37 +structure Basic_Classical: BASIC_CLASSICAL = Classical;
    6.38  open Basic_Classical;
    6.39  *}
    6.40  
    6.41 -setup Classical.setup
    6.42 -
    6.43  setup {*
    6.44 -let
    6.45 -  fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
    6.46 -    | non_bool_eq _ = false;
    6.47 -  fun hyp_subst_tac' ctxt =
    6.48 -    SUBGOAL (fn (goal, i) =>
    6.49 -      if Term.exists_Const non_bool_eq goal
    6.50 -      then Hypsubst.hyp_subst_tac ctxt i
    6.51 -      else no_tac);
    6.52 -in
    6.53 -  Hypsubst.hypsubst_setup
    6.54    (*prevent substitution on bool*)
    6.55 -  #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
    6.56 -end
    6.57 +  let
    6.58 +    fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
    6.59 +      | non_bool_eq _ = false;
    6.60 +    fun hyp_subst_tac' ctxt =
    6.61 +      SUBGOAL (fn (goal, i) =>
    6.62 +        if Term.exists_Const non_bool_eq goal
    6.63 +        then Hypsubst.hyp_subst_tac ctxt i
    6.64 +        else no_tac);
    6.65 +  in
    6.66 +    Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
    6.67 +  end
    6.68  *}
    6.69  
    6.70  declare iffI [intro!]
    6.71 @@ -932,8 +923,6 @@
    6.72    val blast_tac = Blast.blast_tac;
    6.73  *}
    6.74  
    6.75 -setup Blast.setup
    6.76 -
    6.77  
    6.78  subsubsection {* Simplifier *}
    6.79  
    6.80 @@ -1197,18 +1186,14 @@
    6.81  ML_file "Tools/simpdata.ML"
    6.82  ML {* open Simpdata *}
    6.83  
    6.84 -setup {* map_theory_simpset (put_simpset HOL_basic_ss) *}
    6.85 +setup {*
    6.86 +  map_theory_simpset (put_simpset HOL_basic_ss) #>
    6.87 +  Simplifier.method_setup Splitter.split_modifiers
    6.88 +*}
    6.89  
    6.90  simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
    6.91  simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
    6.92  
    6.93 -setup {*
    6.94 -  Simplifier.method_setup Splitter.split_modifiers
    6.95 -  #> Splitter.setup
    6.96 -  #> clasimp_setup
    6.97 -  #> EqSubst.setup
    6.98 -*}
    6.99 -
   6.100  text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *}
   6.101  
   6.102  simproc_setup neq ("x = y") = {* fn _ =>
   6.103 @@ -1467,6 +1452,7 @@
   6.104  
   6.105  text {* Method setup. *}
   6.106  
   6.107 +ML_file "~~/src/Tools/induct.ML"
   6.108  ML {*
   6.109  structure Induct = Induct
   6.110  (
   6.111 @@ -1484,7 +1470,6 @@
   6.112  ML_file "~~/src/Tools/induction.ML"
   6.113  
   6.114  setup {*
   6.115 -  Induct.setup #> Induction.setup #>
   6.116    Context.theory_map (Induct.map_simpset (fn ss => ss
   6.117      addsimprocs
   6.118        [Simplifier.simproc_global @{theory} "swap_induct_false"
   6.119 @@ -1558,13 +1543,12 @@
   6.120  lemma [induct_simp]: "induct_implies induct_true P == P"
   6.121    by (simp add: induct_implies_def induct_true_def)
   6.122  
   6.123 -lemma [induct_simp]: "(x = x) = True" 
   6.124 +lemma [induct_simp]: "(x = x) = True"
   6.125    by (rule simp_thms)
   6.126  
   6.127  hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
   6.128  
   6.129  ML_file "~~/src/Tools/induct_tacs.ML"
   6.130 -setup Induct_Tacs.setup
   6.131  
   6.132  
   6.133  subsubsection {* Coherent logic *}
   6.134 @@ -1640,8 +1624,8 @@
   6.135  lemmas eq_sym_conv = eq_commute
   6.136  
   6.137  lemma nnf_simps:
   6.138 -  "(\<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)" 
   6.139 -  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))" 
   6.140 +  "(\<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)"
   6.141 +  "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
   6.142    "(\<not> \<not>(P)) = P"
   6.143  by blast+
   6.144  
   6.145 @@ -1737,10 +1721,11 @@
   6.146    by (fact arg_cong)
   6.147  
   6.148  setup {*
   6.149 -  Code_Preproc.map_pre (put_simpset HOL_basic_ss)
   6.150 -  #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
   6.151 -  #> Code_Simp.map_ss (put_simpset HOL_basic_ss
   6.152 -    #> Simplifier.add_cong @{thm conj_left_cong} #> Simplifier.add_cong @{thm disj_left_cong})
   6.153 +  Code_Preproc.map_pre (put_simpset HOL_basic_ss) #>
   6.154 +  Code_Preproc.map_post (put_simpset HOL_basic_ss) #>
   6.155 +  Code_Simp.map_ss (put_simpset HOL_basic_ss #>
   6.156 +  Simplifier.add_cong @{thm conj_left_cong} #>
   6.157 +  Simplifier.add_cong @{thm disj_left_cong})
   6.158  *}
   6.159  
   6.160  
   6.161 @@ -1799,7 +1784,7 @@
   6.162  text {* More about @{typ prop} *}
   6.163  
   6.164  lemma [code nbe]:
   6.165 -  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
   6.166 +  shows "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q"
   6.167      and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True"
   6.168      and "(P \<Longrightarrow> R) \<equiv> Trueprop (P \<longrightarrow> R)" by (auto intro!: equal_intr_rule)
   6.169  
   6.170 @@ -1828,9 +1813,7 @@
   6.171    "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
   6.172    by (simp add: equal)
   6.173  
   6.174 -setup {*
   6.175 -  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
   6.176 -*}
   6.177 +setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"}) *}
   6.178  
   6.179  lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
   6.180  proof
   6.181 @@ -1843,14 +1826,10 @@
   6.182    show "PROP ?ofclass" proof
   6.183    qed (simp add: `PROP ?equal`)
   6.184  qed
   6.185 -  
   6.186 -setup {*
   6.187 -  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
   6.188 -*}
   6.189  
   6.190 -setup {*
   6.191 -  Nbe.add_const_alias @{thm equal_alias_cert}
   6.192 -*}
   6.193 +setup {* Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"}) *}
   6.194 +
   6.195 +setup {* Nbe.add_const_alias @{thm equal_alias_cert} *}
   6.196  
   6.197  text {* Cases *}
   6.198  
   6.199 @@ -1860,8 +1839,8 @@
   6.200    using assms by simp_all
   6.201  
   6.202  setup {*
   6.203 -  Code.add_case @{thm Let_case_cert}
   6.204 -  #> Code.add_undefined @{const_name undefined}
   6.205 +  Code.add_case @{thm Let_case_cert} #>
   6.206 +  Code.add_undefined @{const_name undefined}
   6.207  *}
   6.208  
   6.209  declare [[code abort: undefined]]
   6.210 @@ -1877,7 +1856,7 @@
   6.211  | constant True \<rightharpoonup>
   6.212      (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
   6.213  | constant False \<rightharpoonup>
   6.214 -    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" 
   6.215 +    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
   6.216  
   6.217  code_reserved SML
   6.218    bool true false
   6.219 @@ -1936,13 +1915,13 @@
   6.220  subsubsection {* Evaluation and normalization by evaluation *}
   6.221  
   6.222  method_setup eval = {*
   6.223 -let
   6.224 -  fun eval_tac ctxt =
   6.225 -    let val conv = Code_Runtime.dynamic_holds_conv ctxt
   6.226 -    in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
   6.227 -in
   6.228 -  Scan.succeed (SIMPLE_METHOD' o eval_tac)
   6.229 -end
   6.230 +  let
   6.231 +    fun eval_tac ctxt =
   6.232 +      let val conv = Code_Runtime.dynamic_holds_conv ctxt
   6.233 +      in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
   6.234 +  in
   6.235 +    Scan.succeed (SIMPLE_METHOD' o eval_tac)
   6.236 +  end
   6.237  *} "solve goal by evaluation"
   6.238  
   6.239  method_setup normalization = {*
   6.240 @@ -1989,23 +1968,23 @@
   6.241  subsection {* Legacy tactics and ML bindings *}
   6.242  
   6.243  ML {*
   6.244 -(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   6.245 -local
   6.246 -  fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
   6.247 -    | wrong_prem (Bound _) = true
   6.248 -    | wrong_prem _ = false;
   6.249 -  val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
   6.250 -in
   6.251 -  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   6.252 -  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
   6.253 -end;
   6.254 +  (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   6.255 +  local
   6.256 +    fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
   6.257 +      | wrong_prem (Bound _) = true
   6.258 +      | wrong_prem _ = false;
   6.259 +    val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
   6.260 +  in
   6.261 +    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   6.262 +    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
   6.263 +  end;
   6.264  
   6.265 -local
   6.266 -  val nnf_ss =
   6.267 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
   6.268 -in
   6.269 -  fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   6.270 -end
   6.271 +  local
   6.272 +    val nnf_ss =
   6.273 +      simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms simp_thms nnf_simps});
   6.274 +  in
   6.275 +    fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   6.276 +  end
   6.277  *}
   6.278  
   6.279  hide_const (open) eq equal
     7.1 --- a/src/HOL/Orderings.thy	Wed Oct 29 17:01:44 2014 +0100
     7.2 +++ b/src/HOL/Orderings.thy	Wed Oct 29 19:01:49 2014 +0100
     7.3 @@ -400,6 +400,8 @@
     7.4  sig
     7.5    val print_structures: Proof.context -> unit
     7.6    val order_tac: Proof.context -> thm list -> int -> tactic
     7.7 +  val add_struct: string * term list -> string -> attribute
     7.8 +  val del_struct: string * term list -> attribute
     7.9  end;
    7.10  
    7.11  structure Orders: ORDERS =
    7.12 @@ -483,26 +485,24 @@
    7.13  
    7.14  (* attributes *)
    7.15  
    7.16 -fun add_struct_thm s tag =
    7.17 +fun add_struct s tag =
    7.18    Thm.declaration_attribute
    7.19      (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
    7.20  fun del_struct s =
    7.21    Thm.declaration_attribute
    7.22      (fn _ => Data.map (AList.delete struct_eq s));
    7.23  
    7.24 -val _ =
    7.25 -  Theory.setup
    7.26 -    (Attrib.setup @{binding order}
    7.27 -      (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
    7.28 -        Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
    7.29 -        Scan.repeat Args.term
    7.30 -        >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    7.31 -             | ((NONE, n), ts) => del_struct (n, ts)))
    7.32 -      "theorems controlling transitivity reasoner");
    7.33 -
    7.34  end;
    7.35  *}
    7.36  
    7.37 +attribute_setup order = {*
    7.38 +  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
    7.39 +    Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
    7.40 +    Scan.repeat Args.term
    7.41 +    >> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag
    7.42 +         | ((NONE, n), ts) => Orders.del_struct (n, ts))
    7.43 +*} "theorems controlling transitivity reasoner"
    7.44 +
    7.45  method_setup order = {*
    7.46    Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
    7.47  *} "transitivity reasoner"
     8.1 --- a/src/HOL/Product_Type.thy	Wed Oct 29 17:01:44 2014 +0100
     8.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 29 19:01:49 2014 +0100
     8.3 @@ -50,9 +50,7 @@
     8.4    shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
     8.5    using assms by simp_all
     8.6  
     8.7 -setup {*
     8.8 -  Code.add_case @{thm If_case_cert}
     8.9 -*}
    8.10 +setup {* Code.add_case @{thm If_case_cert} *}
    8.11  
    8.12  code_printing
    8.13    constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
     9.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 17:01:44 2014 +0100
     9.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Oct 29 19:01:49 2014 +0100
     9.3 @@ -618,8 +618,6 @@
     9.4  
     9.5  ML_file "Tools/Quickcheck/exhaustive_generators.ML"
     9.6  
     9.7 -setup Exhaustive_Generators.setup
     9.8 -
     9.9  declare [[quickcheck_batch_tester = exhaustive]]
    9.10  
    9.11  subsection {* Defining generators for abstract types *}
    10.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 17:01:44 2014 +0100
    10.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Oct 29 19:01:49 2014 +0100
    10.3 @@ -197,8 +197,6 @@
    10.4  
    10.5  ML_file "Tools/Quickcheck/narrowing_generators.ML"
    10.6  
    10.7 -setup Narrowing_Generators.setup
    10.8 -
    10.9  definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
   10.10  where
   10.11    "narrowing_dummy_partial_term_of = partial_term_of"
    11.1 --- a/src/HOL/Quickcheck_Random.thy	Wed Oct 29 17:01:44 2014 +0100
    11.2 +++ b/src/HOL/Quickcheck_Random.thy	Wed Oct 29 19:01:49 2014 +0100
    11.3 @@ -207,7 +207,6 @@
    11.4  
    11.5  ML_file "Tools/Quickcheck/quickcheck_common.ML" 
    11.6  ML_file "Tools/Quickcheck/random_generators.ML"
    11.7 -setup Random_Generators.setup
    11.8  
    11.9  
   11.10  subsection {* Code setup *}
    12.1 --- a/src/HOL/Semiring_Normalization.thy	Wed Oct 29 17:01:44 2014 +0100
    12.2 +++ b/src/HOL/Semiring_Normalization.thy	Wed Oct 29 19:01:49 2014 +0100
    12.3 @@ -8,8 +8,6 @@
    12.4  imports Numeral_Simprocs Nat_Transfer
    12.5  begin
    12.6  
    12.7 -ML_file "Tools/semiring_normalizer.ML"
    12.8 -
    12.9  text {* Prelude *}
   12.10  
   12.11  class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
   12.12 @@ -69,7 +67,7 @@
   12.13  
   12.14  text {* Semiring normalization proper *}
   12.15  
   12.16 -setup Semiring_Normalizer.setup
   12.17 +ML_file "Tools/semiring_normalizer.ML"
   12.18  
   12.19  context comm_semiring_1
   12.20  begin
    13.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Oct 29 17:01:44 2014 +0100
    13.2 +++ b/src/HOL/Tools/Function/fun.ML	Wed Oct 29 19:01:49 2014 +0100
    13.3 @@ -14,8 +14,6 @@
    13.4    val add_fun_cmd : (binding * string option * mixfix) list ->
    13.5      (Attrib.binding * string) list -> Function_Common.function_config ->
    13.6      bool -> local_theory -> Proof.context
    13.7 -
    13.8 -  val setup : theory -> theory
    13.9  end
   13.10  
   13.11  structure Function_Fun : FUNCTION_FUN =
   13.12 @@ -148,8 +146,8 @@
   13.13    else
   13.14      Function_Common.empty_preproc check_defs config ctxt fixes spec
   13.15  
   13.16 -val setup =
   13.17 -  Context.theory_map (Function_Common.set_preproc sequential_preproc)
   13.18 +val _ = Theory.setup (Context.theory_map (Function_Common.set_preproc sequential_preproc))
   13.19 +
   13.20  
   13.21  
   13.22  val fun_config = FunctionConfig { sequential=true, default=NONE,
    14.1 --- a/src/HOL/Tools/Function/function.ML	Wed Oct 29 17:01:44 2014 +0100
    14.2 +++ b/src/HOL/Tools/Function/function.ML	Wed Oct 29 19:01:49 2014 +0100
    14.3 @@ -32,7 +32,6 @@
    14.4    val termination : term option -> local_theory -> Proof.state
    14.5    val termination_cmd : string option -> local_theory -> Proof.state
    14.6  
    14.7 -  val setup : theory -> theory
    14.8    val get_congs : Proof.context -> thm list
    14.9  
   14.10    val get_info : Proof.context -> term -> info
   14.11 @@ -264,7 +263,6 @@
   14.12  
   14.13  (* Datatype hook to declare datatype congs as "function_congs" *)
   14.14  
   14.15 -
   14.16  fun add_case_cong n thy =
   14.17    let
   14.18      val cong = #case_cong (Old_Datatype_Data.the_info thy n)
   14.19 @@ -274,12 +272,10 @@
   14.20        (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
   14.21    end
   14.22  
   14.23 -val setup_case_cong = Old_Datatype_Data.interpretation (K (fold add_case_cong))
   14.24 +val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
   14.25  
   14.26  
   14.27 -(* setup *)
   14.28 -
   14.29 -val setup = setup_case_cong
   14.30 +(* get info *)
   14.31  
   14.32  val get_congs = Function_Context_Tree.get_function_congs
   14.33  
    15.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Oct 29 17:01:44 2014 +0100
    15.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Oct 29 19:01:49 2014 +0100
    15.3 @@ -21,7 +21,6 @@
    15.4    val quickcheck_pretty : bool Config.T
    15.5    val setup_exhaustive_datatype_interpretation : theory -> theory
    15.6    val setup_bounded_forall_datatype_interpretation : theory -> theory
    15.7 -  val setup: theory -> theory
    15.8    
    15.9    val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
   15.10      (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
   15.11 @@ -547,11 +546,12 @@
   15.12  
   15.13  val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
   15.14  
   15.15 -val setup =
   15.16 -  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
   15.17 -    (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
   15.18 -  #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   15.19 -  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   15.20 -  #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
   15.21 +val _ =
   15.22 +  Theory.setup
   15.23 +   (Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
   15.24 +      (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
   15.25 +    #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   15.26 +    #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   15.27 +    #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)));
   15.28  
   15.29  end;
    16.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Oct 29 17:01:44 2014 +0100
    16.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Oct 29 19:01:49 2014 +0100
    16.3 @@ -16,7 +16,6 @@
    16.4      | Empty_Assignment
    16.5    val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
    16.6    val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
    16.7 -  val setup: theory -> theory
    16.8  end;
    16.9  
   16.10  structure Narrowing_Generators : NARROWING_GENERATORS =
   16.11 @@ -522,11 +521,12 @@
   16.12  
   16.13  val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
   16.14  
   16.15 -val setup =
   16.16 -  Code.datatype_interpretation ensure_partial_term_of
   16.17 -  #> Code.datatype_interpretation ensure_partial_term_of_code
   16.18 -  #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
   16.19 -    (@{sort narrowing}, instantiate_narrowing_datatype)
   16.20 -  #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
   16.21 +val _ =
   16.22 +  Theory.setup
   16.23 +   (Code.datatype_interpretation ensure_partial_term_of
   16.24 +    #> Code.datatype_interpretation ensure_partial_term_of_code
   16.25 +    #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
   16.26 +      (@{sort narrowing}, instantiate_narrowing_datatype)
   16.27 +    #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))));
   16.28      
   16.29  end;
    17.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Oct 29 17:01:44 2014 +0100
    17.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Oct 29 19:01:49 2014 +0100
    17.3 @@ -18,7 +18,6 @@
    17.4      -> Proof.context -> Proof.context
    17.5    val instantiate_random_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
    17.6      (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    17.7 -  val setup: theory -> theory
    17.8  end;
    17.9  
   17.10  structure Random_Generators : RANDOM_GENERATORS =
   17.11 @@ -469,9 +468,10 @@
   17.12  
   17.13  val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
   17.14  
   17.15 -val setup =
   17.16 -  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
   17.17 -    (@{sort random}, instantiate_random_datatype)
   17.18 -  #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
   17.19 +val _ =
   17.20 +  Theory.setup
   17.21 +   (Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
   17.22 +      (@{sort random}, instantiate_random_datatype) #>
   17.23 +    Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals))));
   17.24  
   17.25  end;
    18.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Wed Oct 29 17:01:44 2014 +0100
    18.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Oct 29 19:01:49 2014 +0100
    18.3 @@ -41,8 +41,6 @@
    18.4         main: Proof.context -> conv,
    18.5         pow: Proof.context -> conv,
    18.6         sub: Proof.context -> conv}
    18.7 -
    18.8 -  val setup: theory -> theory
    18.9  end
   18.10  
   18.11  structure Semiring_Normalizer: SEMIRING_NORMALIZER = 
   18.12 @@ -912,20 +910,21 @@
   18.13  
   18.14  in
   18.15  
   18.16 -val setup =
   18.17 -  Attrib.setup @{binding normalizer}
   18.18 -    (Scan.lift (Args.$$$ delN >> K del) ||
   18.19 -      ((keyword2 semiringN opsN |-- terms) --
   18.20 -       (keyword2 semiringN rulesN |-- thms)) --
   18.21 -      (optional (keyword2 ringN opsN |-- terms) --
   18.22 -       optional (keyword2 ringN rulesN |-- thms)) --
   18.23 -      (optional (keyword2 fieldN opsN |-- terms) --
   18.24 -       optional (keyword2 fieldN rulesN |-- thms)) --
   18.25 -      optional (keyword2 idomN rulesN |-- thms) --
   18.26 -      optional (keyword2 idealN rulesN |-- thms)
   18.27 -      >> (fn ((((sr, r), f), id), idl) => 
   18.28 -             add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   18.29 -    "semiring normalizer data";
   18.30 +val _ =
   18.31 +  Theory.setup
   18.32 +    (Attrib.setup @{binding normalizer}
   18.33 +      (Scan.lift (Args.$$$ delN >> K del) ||
   18.34 +        ((keyword2 semiringN opsN |-- terms) --
   18.35 +         (keyword2 semiringN rulesN |-- thms)) --
   18.36 +        (optional (keyword2 ringN opsN |-- terms) --
   18.37 +         optional (keyword2 ringN rulesN |-- thms)) --
   18.38 +        (optional (keyword2 fieldN opsN |-- terms) --
   18.39 +         optional (keyword2 fieldN rulesN |-- thms)) --
   18.40 +        optional (keyword2 idomN rulesN |-- thms) --
   18.41 +        optional (keyword2 idealN rulesN |-- thms)
   18.42 +        >> (fn ((((sr, r), f), id), idl) => 
   18.43 +               add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
   18.44 +      "semiring normalizer data");
   18.45  
   18.46  end;
   18.47  
    19.1 --- a/src/Provers/blast.ML	Wed Oct 29 17:01:44 2014 +0100
    19.2 +++ b/src/Provers/blast.ML	Wed Oct 29 19:01:49 2014 +0100
    19.3 @@ -62,7 +62,6 @@
    19.4    val trace: bool Config.T
    19.5    val stats: bool Config.T
    19.6    val blast_tac: Proof.context -> int -> tactic
    19.7 -  val setup: theory -> theory
    19.8    (*debugging tools*)
    19.9    type branch
   19.10    val tryIt: Proof.context -> int -> string ->
   19.11 @@ -77,7 +76,7 @@
   19.12  
   19.13  (* options *)
   19.14  
   19.15 -val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
   19.16 +val depth_limit = Attrib.setup_config_int @{binding blast_depth_limit} (K 20);
   19.17  val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
   19.18  val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
   19.19  
   19.20 @@ -1294,14 +1293,15 @@
   19.21    in {fullTrace = !fullTrace, result = res} end;
   19.22  
   19.23  
   19.24 +
   19.25  (** method setup **)
   19.26  
   19.27 -val setup =
   19.28 -  setup_depth_limit #>
   19.29 -  Method.setup @{binding blast}
   19.30 -    (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
   19.31 -      (fn NONE => SIMPLE_METHOD' o blast_tac
   19.32 -        | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
   19.33 -    "classical tableau prover";
   19.34 +val _ =
   19.35 +  Theory.setup
   19.36 +    (Method.setup @{binding blast}
   19.37 +      (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
   19.38 +        (fn NONE => SIMPLE_METHOD' o blast_tac
   19.39 +          | SOME lim => (fn ctxt => SIMPLE_METHOD' (depth_tac ctxt lim))))
   19.40 +      "classical tableau prover");
   19.41  
   19.42  end;
    20.1 --- a/src/Provers/clasimp.ML	Wed Oct 29 17:01:44 2014 +0100
    20.2 +++ b/src/Provers/clasimp.ML	Wed Oct 29 19:01:49 2014 +0100
    20.3 @@ -31,7 +31,6 @@
    20.4    val iff_del: attribute
    20.5    val iff_modifiers: Method.modifier parser list
    20.6    val clasimp_modifiers: Method.modifier parser list
    20.7 -  val clasimp_setup: theory -> theory
    20.8  end;
    20.9  
   20.10  functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
   20.11 @@ -180,10 +179,14 @@
   20.12  
   20.13  (* attributes *)
   20.14  
   20.15 -fun iff_att x = (Scan.lift
   20.16 - (Args.del >> K iff_del ||
   20.17 -  Scan.option Args.add -- Args.query >> K iff_add' ||
   20.18 -  Scan.option Args.add >> K iff_add)) x;
   20.19 +val _ =
   20.20 +  Theory.setup
   20.21 +    (Attrib.setup @{binding iff}
   20.22 +      (Scan.lift
   20.23 +        (Args.del >> K iff_del ||
   20.24 +          Scan.option Args.add -- Args.query >> K iff_add' ||
   20.25 +          Scan.option Args.add >> K iff_add))
   20.26 +      "declaration of Simplifier / Classical rules");
   20.27  
   20.28  
   20.29  (* method modifiers *)
   20.30 @@ -211,17 +214,14 @@
   20.31    (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
   20.32      | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
   20.33  
   20.34 -
   20.35 -(* theory setup *)
   20.36 -
   20.37 -val clasimp_setup =
   20.38 -  Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
   20.39 -  Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
   20.40 -  Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
   20.41 -  Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
   20.42 -  Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
   20.43 -  Method.setup @{binding auto} auto_method "auto" #>
   20.44 -  Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
   20.45 -    "clarify simplified goal";
   20.46 +val _ =
   20.47 +  Theory.setup
   20.48 +   (Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
   20.49 +    Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
   20.50 +    Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
   20.51 +    Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
   20.52 +    Method.setup @{binding auto} auto_method "auto" #>
   20.53 +    Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
   20.54 +      "clarify simplified goal");
   20.55  
   20.56  end;
    21.1 --- a/src/Provers/classical.ML	Wed Oct 29 17:01:44 2014 +0100
    21.2 +++ b/src/Provers/classical.ML	Wed Oct 29 19:01:49 2014 +0100
    21.3 @@ -124,7 +124,6 @@
    21.4      (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
    21.5    val cla_method':
    21.6      (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    21.7 -  val setup: theory -> theory
    21.8  end;
    21.9  
   21.10  
   21.11 @@ -882,17 +881,18 @@
   21.12  val elimN = "elim";
   21.13  val destN = "dest";
   21.14  
   21.15 -val setup_attrs =
   21.16 -  Attrib.setup @{binding swapped} (Scan.succeed swapped)
   21.17 -    "classical swap of introduction rule" #>
   21.18 -  Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
   21.19 -    "declaration of Classical destruction rule" #>
   21.20 -  Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
   21.21 -    "declaration of Classical elimination rule" #>
   21.22 -  Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
   21.23 -    "declaration of Classical introduction rule" #>
   21.24 -  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
   21.25 -    "remove declaration of intro/elim/dest rule";
   21.26 +val _ =
   21.27 +  Theory.setup
   21.28 +   (Attrib.setup @{binding swapped} (Scan.succeed swapped)
   21.29 +      "classical swap of introduction rule" #>
   21.30 +    Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
   21.31 +      "declaration of Classical destruction rule" #>
   21.32 +    Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
   21.33 +      "declaration of Classical elimination rule" #>
   21.34 +    Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
   21.35 +      "declaration of Classical introduction rule" #>
   21.36 +    Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
   21.37 +      "remove declaration of intro/elim/dest rule");
   21.38  
   21.39  
   21.40  
   21.41 @@ -941,46 +941,40 @@
   21.42  
   21.43  
   21.44  
   21.45 -(** setup_methods **)
   21.46 +(** method setup **)
   21.47  
   21.48 -val setup_methods =
   21.49 -  Method.setup @{binding default}
   21.50 -   (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
   21.51 -    "apply some intro/elim rule (potentially classical)" #>
   21.52 -  Method.setup @{binding rule}
   21.53 -    (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
   21.54 -    "apply some intro/elim rule (potentially classical)" #>
   21.55 -  Method.setup @{binding contradiction}
   21.56 -    (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
   21.57 -    "proof by contradiction" #>
   21.58 -  Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
   21.59 -    "repeatedly apply safe steps" #>
   21.60 -  Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
   21.61 -  Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
   21.62 -  Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
   21.63 -  Method.setup @{binding deepen}
   21.64 -    (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
   21.65 -      >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
   21.66 -    "classical prover (iterative deepening)" #>
   21.67 -  Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
   21.68 -    "classical prover (apply safe rules)" #>
   21.69 -  Method.setup @{binding safe_step} (cla_method' safe_step_tac)
   21.70 -    "single classical step (safe rules)" #>
   21.71 -  Method.setup @{binding inst_step} (cla_method' inst_step_tac)
   21.72 -    "single classical step (safe rules, allow instantiations)" #>
   21.73 -  Method.setup @{binding step} (cla_method' step_tac)
   21.74 -    "single classical step (safe and unsafe rules)" #>
   21.75 -  Method.setup @{binding slow_step} (cla_method' slow_step_tac)
   21.76 -    "single classical step (safe and unsafe rules, allow backtracking)" #>
   21.77 -  Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
   21.78 -    "single classical step (safe rules, without splitting)";
   21.79 -
   21.80 -
   21.81 -
   21.82 -(** theory setup **)
   21.83 -
   21.84 -val setup = setup_attrs #> setup_methods;
   21.85 -
   21.86 +val _ =
   21.87 +  Theory.setup
   21.88 +   (Method.setup @{binding default}
   21.89 +     (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
   21.90 +      "apply some intro/elim rule (potentially classical)" #>
   21.91 +    Method.setup @{binding rule}
   21.92 +      (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
   21.93 +      "apply some intro/elim rule (potentially classical)" #>
   21.94 +    Method.setup @{binding contradiction}
   21.95 +      (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
   21.96 +      "proof by contradiction" #>
   21.97 +    Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
   21.98 +      "repeatedly apply safe steps" #>
   21.99 +    Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
  21.100 +    Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
  21.101 +    Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
  21.102 +    Method.setup @{binding deepen}
  21.103 +      (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
  21.104 +        >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
  21.105 +      "classical prover (iterative deepening)" #>
  21.106 +    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
  21.107 +      "classical prover (apply safe rules)" #>
  21.108 +    Method.setup @{binding safe_step} (cla_method' safe_step_tac)
  21.109 +      "single classical step (safe rules)" #>
  21.110 +    Method.setup @{binding inst_step} (cla_method' inst_step_tac)
  21.111 +      "single classical step (safe rules, allow instantiations)" #>
  21.112 +    Method.setup @{binding step} (cla_method' step_tac)
  21.113 +      "single classical step (safe and unsafe rules)" #>
  21.114 +    Method.setup @{binding slow_step} (cla_method' slow_step_tac)
  21.115 +      "single classical step (safe and unsafe rules, allow backtracking)" #>
  21.116 +    Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
  21.117 +      "single classical step (safe rules, without splitting)");
  21.118  
  21.119  
  21.120  (** outer syntax **)
    22.1 --- a/src/Provers/hypsubst.ML	Wed Oct 29 17:01:44 2014 +0100
    22.2 +++ b/src/Provers/hypsubst.ML	Wed Oct 29 19:01:49 2014 +0100
    22.3 @@ -52,7 +52,6 @@
    22.4    val hyp_subst_tac          : Proof.context -> int -> tactic
    22.5    val blast_hyp_subst_tac    : bool -> int -> tactic
    22.6    val stac                   : thm -> int -> tactic
    22.7 -  val hypsubst_setup         : theory -> theory
    22.8  end;
    22.9  
   22.10  functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
   22.11 @@ -120,7 +119,7 @@
   22.12                 handle TERM _ => eq_var_aux (k+1) B (A :: hs)
   22.13                   | Match => eq_var_aux (k+1) B (A :: hs))
   22.14        | eq_var_aux k _ _ = raise EQ_VAR
   22.15 -  
   22.16 +
   22.17    in  eq_var_aux 0 t [] end;
   22.18  
   22.19  val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
   22.20 @@ -228,11 +227,10 @@
   22.21      gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
   22.22      if thin then thin_free_eq_tac else K no_tac];
   22.23  
   22.24 -val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool
   22.25 -    @{binding hypsubst_thin} (K false);
   22.26 +val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
   22.27  
   22.28 -fun hyp_subst_tac ctxt = hyp_subst_tac_thin
   22.29 -    (Config.get ctxt hyp_subst_thin) ctxt
   22.30 +fun hyp_subst_tac ctxt =
   22.31 +  hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
   22.32  
   22.33  (*Substitutes for Bound variables only -- this is always safe*)
   22.34  fun bound_hyp_subst_tac ctxt =
   22.35 @@ -296,18 +294,18 @@
   22.36    in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   22.37  
   22.38  
   22.39 -(* theory setup *)
   22.40 +(* method setup *)
   22.41  
   22.42 -val hypsubst_setup =
   22.43 -  Method.setup @{binding hypsubst}
   22.44 -    (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   22.45 -    "substitution using an assumption (improper)" #>
   22.46 -  Method.setup @{binding hypsubst_thin}
   22.47 -    (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   22.48 -        (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   22.49 -    "substitution using an assumption, eliminating assumptions" #>
   22.50 -  hyp_subst_thin_setup #>
   22.51 -  Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   22.52 -    "simple substitution";
   22.53 +val _ =
   22.54 +  Theory.setup
   22.55 +   (Method.setup @{binding hypsubst}
   22.56 +      (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   22.57 +      "substitution using an assumption (improper)" #>
   22.58 +    Method.setup @{binding hypsubst_thin}
   22.59 +      (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   22.60 +          (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   22.61 +      "substitution using an assumption, eliminating assumptions" #>
   22.62 +    Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   22.63 +      "simple substitution");
   22.64  
   22.65  end;
    23.1 --- a/src/Provers/splitter.ML	Wed Oct 29 17:01:44 2014 +0100
    23.2 +++ b/src/Provers/splitter.ML	Wed Oct 29 19:01:49 2014 +0100
    23.3 @@ -37,7 +37,6 @@
    23.4    val split_add: attribute
    23.5    val split_del: attribute
    23.6    val split_modifiers : Method.modifier parser list
    23.7 -  val setup: theory -> theory
    23.8  end;
    23.9  
   23.10  functor Splitter(Data: SPLITTER_DATA): SPLITTER =
   23.11 @@ -453,6 +452,11 @@
   23.12  val split_add = Simplifier.attrib add_split;
   23.13  val split_del = Simplifier.attrib del_split;
   23.14  
   23.15 +val _ =
   23.16 +  Theory.setup
   23.17 +    (Attrib.setup @{binding split}
   23.18 +      (Attrib.add_del split_add split_del) "declare case split rule");
   23.19 +
   23.20  
   23.21  (* methods *)
   23.22  
   23.23 @@ -461,14 +465,10 @@
   23.24    Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
   23.25    Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
   23.26  
   23.27 -
   23.28 -(* theory setup *)
   23.29 -
   23.30 -val setup =
   23.31 -  Attrib.setup @{binding split}
   23.32 -    (Attrib.add_del split_add split_del) "declare case split rule" #>
   23.33 -  Method.setup @{binding split}
   23.34 -    (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
   23.35 -    "apply case split rule";
   23.36 +val _ =
   23.37 +  Theory.setup
   23.38 +    (Method.setup @{binding split}
   23.39 +      (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
   23.40 +      "apply case split rule");
   23.41  
   23.42  end;
    24.1 --- a/src/Tools/case_product.ML	Wed Oct 29 17:01:44 2014 +0100
    24.2 +++ b/src/Tools/case_product.ML	Wed Oct 29 19:01:49 2014 +0100
    24.3 @@ -12,7 +12,7 @@
    24.4  sig
    24.5    val combine: Proof.context -> thm -> thm -> thm
    24.6    val combine_annotated: Proof.context -> thm -> thm -> thm
    24.7 -  val setup: theory -> theory
    24.8 +  val annotation: thm -> thm -> attribute
    24.9  end
   24.10  
   24.11  structure Case_Product: CASE_PRODUCT =
   24.12 @@ -104,15 +104,15 @@
   24.13  
   24.14  (* attribute setup *)
   24.15  
   24.16 -val case_prod_attr =
   24.17 -  let
   24.18 -    fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
   24.19 -  in
   24.20 -    Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
   24.21 -      combine_list (Context.proof_of ctxt) thms thm))
   24.22 -  end
   24.23 -
   24.24 -val setup =
   24.25 -  Attrib.setup @{binding case_product} case_prod_attr "product with other case rules"
   24.26 +val _ =
   24.27 +  Theory.setup
   24.28 +   (Attrib.setup @{binding case_product}
   24.29 +      let
   24.30 +        fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
   24.31 +      in
   24.32 +        Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
   24.33 +          combine_list (Context.proof_of ctxt) thms thm))
   24.34 +      end
   24.35 +    "product with other case rules")
   24.36  
   24.37  end
    25.1 --- a/src/Tools/eqsubst.ML	Wed Oct 29 17:01:44 2014 +0100
    25.2 +++ b/src/Tools/eqsubst.ML	Wed Oct 29 19:01:49 2014 +0100
    25.3 @@ -45,8 +45,6 @@
    25.4    val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
    25.5    val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
    25.6    val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
    25.7 -
    25.8 -  val setup : theory -> theory
    25.9  end;
   25.10  
   25.11  structure EqSubst: EQSUBST =
   25.12 @@ -418,12 +416,12 @@
   25.13  (* combination method that takes a flag (true indicates that subst
   25.14     should be done to an assumption, false = apply to the conclusion of
   25.15     the goal) as well as the theorems to use *)
   25.16 -val setup =
   25.17 -  Method.setup @{binding subst}
   25.18 -    (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
   25.19 -        Attrib.thms >>
   25.20 -      (fn ((asm, occs), inthms) => fn ctxt =>
   25.21 -        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
   25.22 -    "single-step substitution";
   25.23 +val _ =
   25.24 +  Theory.setup
   25.25 +    (Method.setup @{binding subst}
   25.26 +      (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
   25.27 +        Attrib.thms >> (fn ((asm, occs), inthms) => fn ctxt =>
   25.28 +          SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
   25.29 +      "single-step substitution");
   25.30  
   25.31  end;
    26.1 --- a/src/Tools/induct.ML	Wed Oct 29 17:01:44 2014 +0100
    26.2 +++ b/src/Tools/induct.ML	Wed Oct 29 19:01:49 2014 +0100
    26.3 @@ -89,7 +89,6 @@
    26.4      (string * typ) list list -> term option list -> thm list option ->
    26.5      thm list -> int -> cases_tactic) ->
    26.6     theory -> theory
    26.7 -  val setup: theory -> theory
    26.8  end;
    26.9  
   26.10  functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
   26.11 @@ -368,15 +367,16 @@
   26.12  
   26.13  in
   26.14  
   26.15 -val attrib_setup =
   26.16 -  Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
   26.17 -    "declaration of cases rule" #>
   26.18 -  Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
   26.19 -    "declaration of induction rule" #>
   26.20 -  Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
   26.21 -    "declaration of coinduction rule" #>
   26.22 -  Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
   26.23 -    "declaration of rules for simplifying induction or cases rules";
   26.24 +val _ =
   26.25 +  Theory.setup
   26.26 +   (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
   26.27 +      "declaration of cases rule" #>
   26.28 +    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
   26.29 +      "declaration of induction rule" #>
   26.30 +    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
   26.31 +      "declaration of coinduction rule" #>
   26.32 +    Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
   26.33 +      "declaration of rules for simplifying induction or cases rules");
   26.34  
   26.35  end;
   26.36  
   26.37 @@ -923,14 +923,15 @@
   26.38  
   26.39  in
   26.40  
   26.41 -val cases_setup =
   26.42 -  Method.setup @{binding cases}
   26.43 -    (Scan.lift (Args.mode no_simpN) --
   26.44 -      (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   26.45 -      (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
   26.46 -        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
   26.47 -          (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
   26.48 -    "case analysis on types or predicates/sets";
   26.49 +val _ =
   26.50 +  Theory.setup
   26.51 +    (Method.setup @{binding cases}
   26.52 +      (Scan.lift (Args.mode no_simpN) --
   26.53 +        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   26.54 +        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
   26.55 +          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
   26.56 +            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
   26.57 +      "case analysis on types or predicates/sets");
   26.58  
   26.59  fun gen_induct_setup binding tac =
   26.60    Method.setup binding
   26.61 @@ -941,21 +942,16 @@
   26.62          Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
   26.63      "induction on types or predicates/sets";
   26.64  
   26.65 -val induct_setup = gen_induct_setup @{binding induct} induct_tac;
   26.66 +val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
   26.67  
   26.68 -val coinduct_setup =
   26.69 -  Method.setup @{binding coinduct}
   26.70 -    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
   26.71 -      (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
   26.72 -        Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
   26.73 -    "coinduction on types or predicates/sets";
   26.74 +val _ =
   26.75 +  Theory.setup
   26.76 +    (Method.setup @{binding coinduct}
   26.77 +      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
   26.78 +        (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
   26.79 +          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
   26.80 +      "coinduction on types or predicates/sets");
   26.81  
   26.82  end;
   26.83  
   26.84 -
   26.85 -
   26.86 -(** theory setup **)
   26.87 -
   26.88 -val setup = attrib_setup #> cases_setup  #> induct_setup #> coinduct_setup;
   26.89 -
   26.90  end;
    27.1 --- a/src/Tools/induct_tacs.ML	Wed Oct 29 17:01:44 2014 +0100
    27.2 +++ b/src/Tools/induct_tacs.ML	Wed Oct 29 19:01:49 2014 +0100
    27.3 @@ -10,7 +10,6 @@
    27.4    val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
    27.5    val induct_tac: Proof.context -> string option list list -> int -> tactic
    27.6    val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
    27.7 -  val setup: theory -> theory
    27.8  end
    27.9  
   27.10  structure Induct_Tacs: INDUCT_TACS =
   27.11 @@ -128,15 +127,16 @@
   27.12  
   27.13  in
   27.14  
   27.15 -val setup =
   27.16 -  Method.setup @{binding case_tac}
   27.17 -    (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
   27.18 -      (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
   27.19 -    "unstructured case analysis on types" #>
   27.20 -  Method.setup @{binding induct_tac}
   27.21 -    (Args.goal_spec -- varss -- opt_rules >>
   27.22 -      (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
   27.23 -    "unstructured induction on types";
   27.24 +val _ =
   27.25 +  Theory.setup
   27.26 +   (Method.setup @{binding case_tac}
   27.27 +      (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
   27.28 +        (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
   27.29 +      "unstructured case analysis on types" #>
   27.30 +    Method.setup @{binding induct_tac}
   27.31 +      (Args.goal_spec -- varss -- opt_rules >>
   27.32 +        (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
   27.33 +      "unstructured induction on types");
   27.34  
   27.35  end;
   27.36  
    28.1 --- a/src/Tools/induction.ML	Wed Oct 29 17:01:44 2014 +0100
    28.2 +++ b/src/Tools/induction.ML	Wed Oct 29 19:01:49 2014 +0100
    28.3 @@ -3,7 +3,6 @@
    28.4    val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    28.5      (string * typ) list list -> term option list -> thm list option ->
    28.6      thm list -> int -> cases_tactic
    28.7 -  val setup: theory -> theory
    28.8  end
    28.9  
   28.10  structure Induction: INDUCTION =
   28.11 @@ -37,7 +36,7 @@
   28.12  
   28.13  val induction_tac = Induct.gen_induct_tac (K name_hyps)
   28.14  
   28.15 -val setup = Induct.gen_induct_setup @{binding induction} induction_tac
   28.16 +val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
   28.17  
   28.18  end
   28.19  
    29.1 --- a/src/Tools/subtyping.ML	Wed Oct 29 17:01:44 2014 +0100
    29.2 +++ b/src/Tools/subtyping.ML	Wed Oct 29 19:01:49 2014 +0100
    29.3 @@ -10,7 +10,6 @@
    29.4    val add_type_map: term -> Context.generic -> Context.generic
    29.5    val add_coercion: term -> Context.generic -> Context.generic
    29.6    val print_coercions: Proof.context -> unit
    29.7 -  val setup: theory -> theory
    29.8  end;
    29.9  
   29.10  structure Subtyping: SUBTYPING =
   29.11 @@ -884,9 +883,11 @@
   29.12  
   29.13  val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
   29.14  
   29.15 -val add_term_check =
   29.16 -  Syntax_Phases.term_check ~100 "coercions"
   29.17 -    (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt);
   29.18 +val _ =
   29.19 +  Theory.setup
   29.20 +    (Context.theory_map
   29.21 +      (Syntax_Phases.term_check ~100 "coercions"
   29.22 +        (fn ctxt => Config.get ctxt coercion_enabled ? coercion_infer_types ctxt)));
   29.23  
   29.24  
   29.25  (* declarations *)
   29.26 @@ -1088,26 +1089,26 @@
   29.27    end |> Pretty.writeln_chunks;
   29.28  
   29.29  
   29.30 -(* theory setup *)
   29.31 +(* attribute setup *)
   29.32  
   29.33  val parse_coerce_args =
   29.34    Args.$$$ "+" >> K PERMIT || Args.$$$ "-" >> K FORBID || Args.$$$ "0" >> K LEAVE
   29.35  
   29.36 -val setup =
   29.37 -  Context.theory_map add_term_check #>
   29.38 -  Attrib.setup @{binding coercion}
   29.39 -    (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
   29.40 -    "declaration of new coercions" #>
   29.41 -  Attrib.setup @{binding coercion_delete}
   29.42 -    (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
   29.43 -    "deletion of coercions" #>
   29.44 -  Attrib.setup @{binding coercion_map}
   29.45 -    (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
   29.46 -    "declaration of new map functions" #>
   29.47 -  Attrib.setup @{binding coercion_args}
   29.48 -    (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
   29.49 -      (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
   29.50 -    "declaration of new constants with coercion-invariant arguments";
   29.51 +val _ =
   29.52 +  Theory.setup
   29.53 +   (Attrib.setup @{binding coercion}
   29.54 +      (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
   29.55 +      "declaration of new coercions" #>
   29.56 +    Attrib.setup @{binding coercion_delete}
   29.57 +      (Args.term >> (fn t => Thm.declaration_attribute (K (delete_coercion t))))
   29.58 +      "deletion of coercions" #>
   29.59 +    Attrib.setup @{binding coercion_map}
   29.60 +      (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
   29.61 +      "declaration of new map functions" #>
   29.62 +    Attrib.setup @{binding coercion_args}
   29.63 +      (Args.const {proper = false, strict = false} -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
   29.64 +        (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
   29.65 +      "declaration of new constants with coercion-invariant arguments");
   29.66  
   29.67  
   29.68  (* outer syntax commands *)