setup: theory -> theory;
authorwenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 187084b3dadb4fe33
parent 18707 9d6154f76476
child 18709 f174ebc26073
setup: theory -> theory;
doc-src/LaTeXsugar/Sugar/Sugar.thy
src/FOL/IFOL.thy
src/FOL/cladata.ML
src/FOL/simpdata.ML
src/HOL/Extraction.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/StarDef.thy
src/HOL/Hyperreal/hypreal_arith.ML
src/HOL/Hyperreal/transfer.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_package.ML
src/HOL/Import/shuffler.ML
src/HOL/Integ/IntDef.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Integ/presburger.ML
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/comm_ring.ML
src/HOL/Library/word_setup.ML
src/HOL/List.thy
src/HOL/Product_Type.thy
src/HOL/Real/rat_arith.ML
src/HOL/Real/real_arith.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/reconstruction.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_atp_methods.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/split_rule.ML
src/HOL/Tools/typedef_package.ML
src/HOL/antisym_setup.ML
src/HOL/arith_data.ML
src/HOL/cladata.ML
src/HOL/simpdata.ML
src/HOLCF/cont_proc.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/eqsubst.ML
src/Provers/hypsubst.ML
src/Provers/induct_method.ML
src/Provers/splitter.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/skip_proof.ML
src/Pure/Isar/term_style.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/compute.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/proof_general.ML
src/Pure/simplifier.ML
src/Sequents/prover.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/numeral_syntax.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -389,7 +389,7 @@
     1.4  setup {*
     1.5  let
     1.6    fun my_concl ctxt = Logic.strip_imp_concl
     1.7 -  in [TermStyle.add_style "my_concl" my_concl]
     1.8 +  in TermStyle.add_style "my_concl" my_concl
     1.9  end;
    1.10  *}
    1.11  (*>*)
    1.12 @@ -399,7 +399,7 @@
    1.13      \verb!setup {!\verb!*!\\
    1.14      \verb!let!\\
    1.15      \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
    1.16 -    \verb!  in [TermStyle.add_style "my_concl" my_concl]!\\
    1.17 +    \verb!  in TermStyle.add_style "my_concl" my_concl!\\
    1.18      \verb!end;!\\
    1.19      \verb!*!\verb!}!\\
    1.20    \end{quote}
     2.1 --- a/src/FOL/IFOL.thy	Thu Jan 19 15:45:10 2006 +0100
     2.2 +++ b/src/FOL/IFOL.thy	Thu Jan 19 21:22:08 2006 +0100
     2.3 @@ -194,9 +194,7 @@
     2.4    and [Pure.elim 2] = allE notE' impE'
     2.5    and [Pure.intro] = exI disjI2 disjI1
     2.6  
     2.7 -setup {*
     2.8 -  [ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)]
     2.9 -*}
    2.10 +setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
    2.11  
    2.12  
    2.13  lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
     3.1 --- a/src/FOL/cladata.ML	Thu Jan 19 15:45:10 2006 +0100
     3.2 +++ b/src/FOL/cladata.ML	Thu Jan 19 21:22:08 2006 +0100
     3.3 @@ -42,9 +42,9 @@
     3.4  val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
     3.5                       addSEs [exE,alt_ex1E] addEs [allE];
     3.6  
     3.7 -val cla_setup = [fn thy => (change_claset_of thy (fn _ => FOL_cs); thy)];
     3.8 +val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
     3.9  
    3.10  val case_setup =
    3.11 - [Method.add_methods
    3.12 + (Method.add_methods
    3.13      [("case_tac", Method.goal_args Args.name case_tac,
    3.14 -      "case_tac emulation (dynamic instantiation!)")]];
    3.15 +      "case_tac emulation (dynamic instantiation!)")]);
     4.1 --- a/src/FOL/simpdata.ML	Thu Jan 19 15:45:10 2006 +0100
     4.2 +++ b/src/FOL/simpdata.ML	Thu Jan 19 21:22:08 2006 +0100
     4.3 @@ -361,7 +361,7 @@
     4.4  (*classical simprules too*)
     4.5  val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
     4.6  
     4.7 -val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
     4.8 +val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
     4.9  
    4.10  
    4.11  (*** integration of simplifier with classical reasoner ***)
     5.1 --- a/src/HOL/Extraction.thy	Thu Jan 19 15:45:10 2006 +0100
     5.2 +++ b/src/HOL/Extraction.thy	Thu Jan 19 21:22:08 2006 +0100
     5.3 @@ -35,16 +35,16 @@
     5.4      incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
     5.5        Bound 0 $ incr_boundvars 1 s));
     5.6  in
     5.7 -  [Extraction.add_types
     5.8 +  Extraction.add_types
     5.9        [("bool", ([], NONE)),
    5.10 -       ("set", ([realizes_set_proc], SOME mk_realizes_set))],
    5.11 -    Extraction.set_preprocessor (fn thy =>
    5.12 +       ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
    5.13 +  Extraction.set_preprocessor (fn thy =>
    5.14        Proofterm.rewrite_proof_notypes
    5.15          ([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
    5.16            ProofRewriteRules.rprocs true) o
    5.17        Proofterm.rewrite_proof thy
    5.18          (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
    5.19 -      ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    5.20 +      ProofRewriteRules.elim_vars (curry Const "arbitrary"))
    5.21  end
    5.22  *}
    5.23  
     6.1 --- a/src/HOL/HOL.thy	Thu Jan 19 15:45:10 2006 +0100
     6.2 +++ b/src/HOL/HOL.thy	Thu Jan 19 21:22:08 2006 +0100
     6.3 @@ -911,9 +911,7 @@
     6.4  use "cladata.ML"
     6.5  setup hypsubst_setup
     6.6  
     6.7 -setup {*
     6.8 -  [ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)]
     6.9 -*}
    6.10 +setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
    6.11  
    6.12  setup Classical.setup
    6.13  setup clasetup
    6.14 @@ -1233,7 +1231,7 @@
    6.15  
    6.16  in
    6.17  
    6.18 -val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
    6.19 +val eq_codegen_setup = Codegen.add_codegen "eq_codegen" eq_codegen;
    6.20  
    6.21  end;
    6.22  *}
     7.1 --- a/src/HOL/Hyperreal/StarDef.thy	Thu Jan 19 15:45:10 2006 +0100
     7.2 +++ b/src/HOL/Hyperreal/StarDef.thy	Thu Jan 19 21:22:08 2006 +0100
     7.3 @@ -161,7 +161,7 @@
     7.4    "star_of x \<equiv> star_n (\<lambda>n. x)"
     7.5  
     7.6  text {* Transfer tactic should remove occurrences of @{term star_of} *}
     7.7 -setup {* [Transfer.add_const "StarDef.star_of"] *}
     7.8 +setup {* Transfer.add_const "StarDef.star_of" *}
     7.9  declare star_of_def [transfer_intro]
    7.10  
    7.11  lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
    7.12 @@ -184,7 +184,7 @@
    7.13      UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
    7.14  
    7.15  text {* Transfer tactic should remove occurrences of @{term Ifun} *}
    7.16 -setup {* [Transfer.add_const "StarDef.Ifun"] *}
    7.17 +setup {* Transfer.add_const "StarDef.Ifun" *}
    7.18  
    7.19  lemma transfer_Ifun [transfer_intro]:
    7.20    "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
    7.21 @@ -234,7 +234,7 @@
    7.22  by (simp add: unstar_def star_of_inject)
    7.23  
    7.24  text {* Transfer tactic should remove occurrences of @{term unstar} *}
    7.25 -setup {* [Transfer.add_const "StarDef.unstar"] *}
    7.26 +setup {* Transfer.add_const "StarDef.unstar" *}
    7.27  
    7.28  lemma transfer_unstar [transfer_intro]:
    7.29    "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
    7.30 @@ -277,7 +277,7 @@
    7.31  by (simp add: Iset_def starP2_star_n)
    7.32  
    7.33  text {* Transfer tactic should remove occurrences of @{term Iset} *}
    7.34 -setup {* [Transfer.add_const "StarDef.Iset"] *}
    7.35 +setup {* Transfer.add_const "StarDef.Iset" *}
    7.36  
    7.37  lemma transfer_mem [transfer_intro]:
    7.38    "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
     8.1 --- a/src/HOL/Hyperreal/hypreal_arith.ML	Thu Jan 19 15:45:10 2006 +0100
     8.2 +++ b/src/HOL/Hyperreal/hypreal_arith.ML	Thu Jan 19 21:22:08 2006 +0100
     8.3 @@ -28,15 +28,15 @@
     8.4      Fast_Arith.lin_arith_prover;
     8.5  
     8.6  val hypreal_arith_setup =
     8.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     8.8 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     8.9     {add_mono_thms = add_mono_thms,
    8.10      mult_mono_thms = mult_mono_thms,
    8.11      inj_thms = inj_thms @ real_inj_thms, 
    8.12      lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
    8.13      neqE = neqE,
    8.14 -    simpset = simpset}),
    8.15 -  arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT),
    8.16 -  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy)];
    8.17 +    simpset = simpset}) #>
    8.18 +  arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
    8.19 +  (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy));
    8.20  
    8.21  end;
    8.22  
     9.1 --- a/src/HOL/Hyperreal/transfer.ML	Thu Jan 19 15:45:10 2006 +0100
     9.2 +++ b/src/HOL/Hyperreal/transfer.ML	Thu Jan 19 21:22:08 2006 +0100
     9.3 @@ -9,7 +9,7 @@
     9.4  sig
     9.5    val transfer_tac: thm list -> int -> tactic
     9.6    val add_const: string -> theory -> theory
     9.7 -  val setup: (theory -> theory) list
     9.8 +  val setup: theory -> theory
     9.9  end;
    9.10  
    9.11  structure Transfer: TRANSFER_TAC =
    9.12 @@ -127,17 +127,15 @@
    9.13  val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
    9.14  
    9.15  val setup =
    9.16 -  [ TransferData.init,
    9.17 -    Attrib.add_attributes
    9.18 -    [ ("transfer_intro", intro_attr,
    9.19 -       "declaration of transfer introduction rule"),
    9.20 -      ("transfer_unfold", unfold_attr,
    9.21 -       "declaration of transfer unfolding rule"),
    9.22 -      ("transfer_refold", refold_attr,
    9.23 -       "declaration of transfer refolding rule")
    9.24 -    ],
    9.25 -    Method.add_method
    9.26 -    ("transfer", Method.thms_args transfer_method, "transfer principle")
    9.27 -  ];
    9.28 +  TransferData.init #>
    9.29 +  Attrib.add_attributes
    9.30 +    [("transfer_intro", intro_attr,
    9.31 +      "declaration of transfer introduction rule"),
    9.32 +     ("transfer_unfold", unfold_attr,
    9.33 +      "declaration of transfer unfolding rule"),
    9.34 +     ("transfer_refold", refold_attr,
    9.35 +      "declaration of transfer refolding rule")] #>
    9.36 +  Method.add_method
    9.37 +    ("transfer", Method.thms_args transfer_method, "transfer principle");
    9.38  
    9.39  end;
    10.1 --- a/src/HOL/Import/hol4rews.ML	Thu Jan 19 15:45:10 2006 +0100
    10.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Jan 19 21:22:08 2006 +0100
    10.3 @@ -758,24 +758,25 @@
    10.4  	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
    10.5  in
    10.6  val hol4_setup =
    10.7 -    [HOL4Rewrites.init,
    10.8 -     HOL4Maps.init,
    10.9 -     HOL4UNames.init,
   10.10 -     HOL4DefMaps.init,
   10.11 -     HOL4Moves.init,
   10.12 -     HOL4CMoves.init,
   10.13 -     HOL4ConstMaps.init,
   10.14 -     HOL4Rename.init,
   10.15 -     HOL4TypeMaps.init,
   10.16 -     HOL4Pending.init,
   10.17 -     HOL4Thms.init,
   10.18 -     HOL4Dump.init,
   10.19 -     HOL4DefThy.init,
   10.20 -     HOL4Imports.init,
   10.21 -     ImportSegment.init,
   10.22 -     initial_maps,
   10.23 -     Attrib.add_attributes [("hol4rew",
   10.24 -			     (Attrib.no_args add_hol4_rewrite,
   10.25 -			      Attrib.no_args Attrib.undef_local_attribute),
   10.26 -			     "HOL4 rewrite rule")]]
   10.27 +  HOL4Rewrites.init #>
   10.28 +  HOL4Maps.init #>
   10.29 +  HOL4UNames.init #>
   10.30 +  HOL4DefMaps.init #>
   10.31 +  HOL4Moves.init #>
   10.32 +  HOL4CMoves.init #>
   10.33 +  HOL4ConstMaps.init #>
   10.34 +  HOL4Rename.init #>
   10.35 +  HOL4TypeMaps.init #>
   10.36 +  HOL4Pending.init #>
   10.37 +  HOL4Thms.init #>
   10.38 +  HOL4Dump.init #>
   10.39 +  HOL4DefThy.init #>
   10.40 +  HOL4Imports.init #>
   10.41 +  ImportSegment.init #>
   10.42 +  initial_maps #>
   10.43 +  Attrib.add_attributes
   10.44 +    [("hol4rew",
   10.45 +      (Attrib.no_args add_hol4_rewrite,
   10.46 +       Attrib.no_args Attrib.undef_local_attribute),
   10.47 +      "HOL4 rewrite rule")]
   10.48  end
    11.1 --- a/src/HOL/Import/import_package.ML	Thu Jan 19 15:45:10 2006 +0100
    11.2 +++ b/src/HOL/Import/import_package.ML	Thu Jan 19 21:22:08 2006 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  signature IMPORT_PACKAGE =
    11.5  sig
    11.6      val import_meth: Method.src -> Proof.context -> Proof.method
    11.7 -    val setup      : (theory -> theory) list
    11.8 +    val setup      : theory -> theory
    11.9      val debug      : bool ref
   11.10  end
   11.11  
   11.12 @@ -80,6 +80,6 @@
   11.13  			  Method.SIMPLE_METHOD (import_tac arg thy)
   11.14  		      end)
   11.15  
   11.16 -val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init]
   11.17 +val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
   11.18  end
   11.19  
    12.1 --- a/src/HOL/Import/shuffler.ML	Thu Jan 19 15:45:10 2006 +0100
    12.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jan 19 21:22:08 2006 +0100
    12.3 @@ -26,7 +26,7 @@
    12.4      val add_shuffle_rule: thm -> theory -> theory
    12.5      val shuffle_attr: theory attribute
    12.6  
    12.7 -    val setup      : (theory -> theory) list
    12.8 +    val setup      : theory -> theory
    12.9  end
   12.10  
   12.11  structure Shuffler :> Shuffler =
   12.12 @@ -684,13 +684,15 @@
   12.13  
   12.14  fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm)
   12.15  
   12.16 -val setup = [Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around"),
   12.17 -	     Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems"),
   12.18 -	     ShuffleData.init,
   12.19 -	     add_shuffle_rule weaken,
   12.20 -	     add_shuffle_rule equiv_comm,
   12.21 -	     add_shuffle_rule imp_comm,
   12.22 -	     add_shuffle_rule Drule.norm_hhf_eq,
   12.23 -	     add_shuffle_rule Drule.triv_forall_equality,
   12.24 -	     Attrib.add_attributes [("shuffle_rule",(Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]]
   12.25 +val setup =
   12.26 +  Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
   12.27 +  Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
   12.28 +  ShuffleData.init #>
   12.29 +  add_shuffle_rule weaken #>
   12.30 +  add_shuffle_rule equiv_comm #>
   12.31 +  add_shuffle_rule imp_comm #>
   12.32 +  add_shuffle_rule Drule.norm_hhf_eq #>
   12.33 +  add_shuffle_rule Drule.triv_forall_equality #>
   12.34 +  Attrib.add_attributes [("shuffle_rule", (Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]
   12.35 +
   12.36  end
    13.1 --- a/src/HOL/Integ/IntDef.thy	Thu Jan 19 15:45:10 2006 +0100
    13.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Jan 19 21:22:08 2006 +0100
    13.3 @@ -948,12 +948,12 @@
    13.4  
    13.5  *}
    13.6  
    13.7 -setup {*[
    13.8 -  Codegen.add_codegen "number_of_codegen" number_of_codegen,
    13.9 +setup {*
   13.10 +  Codegen.add_codegen "number_of_codegen" number_of_codegen #>
   13.11    CodegenPackage.add_appconst
   13.12 -    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")),
   13.13 +    ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")) #>
   13.14    CodegenPackage.set_int_tyco "IntDef.int"
   13.15 -]*}
   13.16 +*}
   13.17  
   13.18  quickcheck_params [default_type = int]
   13.19  
    14.1 --- a/src/HOL/Integ/NatBin.thy	Thu Jan 19 15:45:10 2006 +0100
    14.2 +++ b/src/HOL/Integ/NatBin.thy	Thu Jan 19 21:22:08 2006 +0100
    14.3 @@ -591,14 +591,14 @@
    14.4  val numeral_ss = simpset() addsimps numerals;
    14.5  
    14.6  val nat_bin_arith_setup =
    14.7 - [Fast_Arith.map_data 
    14.8 + Fast_Arith.map_data
    14.9     (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   14.10       {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   14.11        inj_thms = inj_thms,
   14.12        lessD = lessD, neqE = neqE,
   14.13        simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
   14.14                                    not_neg_number_of_Pls,
   14.15 -                                  neg_number_of_Min,neg_number_of_BIT]})]
   14.16 +                                  neg_number_of_Min,neg_number_of_BIT]})
   14.17  *}
   14.18  
   14.19  setup nat_bin_arith_setup
    15.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Jan 19 15:45:10 2006 +0100
    15.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Jan 19 21:22:08 2006 +0100
    15.3 @@ -521,7 +521,7 @@
    15.4  in
    15.5  
    15.6  val int_arith_setup =
    15.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    15.8 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    15.9     {add_mono_thms = add_mono_thms,
   15.10      mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
   15.11      inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
   15.12 @@ -529,10 +529,10 @@
   15.13      neqE = thm "linorder_neqE_int" :: neqE,
   15.14      simpset = simpset addsimps add_rules
   15.15                        addsimprocs simprocs
   15.16 -                      addcongs [if_weak_cong]}),
   15.17 -  arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT),
   15.18 -  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
   15.19 -  arith_discrete "IntDef.int"];
   15.20 +                      addcongs [if_weak_cong]}) #>
   15.21 +  arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT) #>
   15.22 +  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
   15.23 +  arith_discrete "IntDef.int";
   15.24  
   15.25  end;
   15.26  
    16.1 --- a/src/HOL/Integ/nat_simprocs.ML	Thu Jan 19 15:45:10 2006 +0100
    16.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Thu Jan 19 21:22:08 2006 +0100
    16.3 @@ -554,10 +554,10 @@
    16.4  in
    16.5  
    16.6  val nat_simprocs_setup =
    16.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    16.8 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    16.9     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   16.10      inj_thms = inj_thms, lessD = lessD, neqE = neqE,
   16.11      simpset = simpset addsimps add_rules
   16.12 -                      addsimprocs simprocs})];
   16.13 +                      addsimprocs simprocs});
   16.14  
   16.15  end;
    17.1 --- a/src/HOL/Integ/presburger.ML	Thu Jan 19 15:45:10 2006 +0100
    17.2 +++ b/src/HOL/Integ/presburger.ML	Thu Jan 19 21:22:08 2006 +0100
    17.3 @@ -14,7 +14,7 @@
    17.4  sig
    17.5   val presburger_tac : bool -> bool -> int -> tactic
    17.6   val presburger_method : bool -> bool -> int -> Proof.method
    17.7 - val setup : (theory -> theory) list
    17.8 + val setup : theory -> theory
    17.9   val trace : bool ref
   17.10  end;
   17.11  
   17.12 @@ -364,12 +364,12 @@
   17.13    Method.insert_tac facts 1 THEN presburger_tac q a i)
   17.14  
   17.15  val setup =
   17.16 -  [Method.add_method ("presburger",
   17.17 -     presburger_args presburger_method,
   17.18 -     "decision procedure for Presburger arithmetic"),
   17.19 -   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
   17.20 -     {splits = splits, inj_consts = inj_consts, discrete = discrete,
   17.21 -      presburger = SOME (presburger_tac true true)})];
   17.22 +  Method.add_method ("presburger",
   17.23 +    presburger_args presburger_method,
   17.24 +    "decision procedure for Presburger arithmetic") #>
   17.25 +  ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
   17.26 +    {splits = splits, inj_consts = inj_consts, discrete = discrete,
   17.27 +      presburger = SOME (presburger_tac true true)});
   17.28  
   17.29  end;
   17.30  
    18.1 --- a/src/HOL/Library/Commutative_Ring.thy	Thu Jan 19 15:45:10 2006 +0100
    18.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Thu Jan 19 21:22:08 2006 +0100
    18.3 @@ -322,6 +322,6 @@
    18.4  generate_code ("ring.ML") test = "norm"*)
    18.5  
    18.6  use "comm_ring.ML"
    18.7 -setup "CommRing.setup"
    18.8 +setup CommRing.setup
    18.9  
   18.10  end
    19.1 --- a/src/HOL/Library/EfficientNat.thy	Thu Jan 19 15:45:10 2006 +0100
    19.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu Jan 19 21:22:08 2006 +0100
    19.3 @@ -222,8 +222,8 @@
    19.4    end;
    19.5  
    19.6  val suc_preproc_setup =
    19.7 -  [Codegen.add_preprocessor eqn_suc_preproc,
    19.8 -   Codegen.add_preprocessor clause_suc_preproc];
    19.9 +  Codegen.add_preprocessor eqn_suc_preproc #>
   19.10 +  Codegen.add_preprocessor clause_suc_preproc;
   19.11  *}
   19.12  
   19.13  setup suc_preproc_setup
    20.1 --- a/src/HOL/Library/comm_ring.ML	Thu Jan 19 15:45:10 2006 +0100
    20.2 +++ b/src/HOL/Library/comm_ring.ML	Thu Jan 19 21:22:08 2006 +0100
    20.3 @@ -9,7 +9,7 @@
    20.4    val comm_ring_tac : int -> tactic
    20.5    val comm_ring_method: int -> Proof.method
    20.6    val algebra_method: int -> Proof.method
    20.7 -  val setup : (theory -> theory) list
    20.8 +  val setup : theory -> theory
    20.9  end
   20.10  
   20.11  structure CommRing: COMM_RING =
   20.12 @@ -132,11 +132,11 @@
   20.13  val algebra_method = comm_ring_method;
   20.14  
   20.15  val setup =
   20.16 -  [Method.add_method ("comm_ring",
   20.17 +  Method.add_method ("comm_ring",
   20.18       Method.no_args (comm_ring_method 1),
   20.19 -     "reflective decision procedure for equalities over commutative rings"),
   20.20 -   Method.add_method ("algebra",
   20.21 +     "reflective decision procedure for equalities over commutative rings") #>
   20.22 +  Method.add_method ("algebra",
   20.23       Method.no_args (algebra_method 1),
   20.24 -     "Method for proving algebraic properties: for now only comm_ring")];
   20.25 +     "Method for proving algebraic properties: for now only comm_ring");
   20.26  
   20.27  end;
    21.1 --- a/src/HOL/Library/word_setup.ML	Thu Jan 19 15:45:10 2006 +0100
    21.2 +++ b/src/HOL/Library/word_setup.ML	Thu Jan 19 21:22:08 2006 +0100
    21.3 @@ -42,5 +42,5 @@
    21.4            thy
    21.5  	end
    21.6  in
    21.7 -val setup_word = [add_word]
    21.8 +val setup_word = add_word
    21.9  end
    22.1 --- a/src/HOL/List.thy	Thu Jan 19 15:45:10 2006 +0100
    22.2 +++ b/src/HOL/List.thy	Thu Jan 19 21:22:08 2006 +0100
    22.3 @@ -2652,14 +2652,12 @@
    22.4  
    22.5  in
    22.6  
    22.7 -val list_codegen_setup = [
    22.8 -  Codegen.add_codegen "list_codegen" list_codegen,
    22.9 -  Codegen.add_codegen "char_codegen" char_codegen,
   22.10 +val list_codegen_setup =
   22.11 +  Codegen.add_codegen "list_codegen" list_codegen #>
   22.12 +  Codegen.add_codegen "char_codegen" char_codegen #>
   22.13    fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
   22.14      ("ml", (7, "::")),
   22.15 -    ("haskell", (5, ":")) 
   22.16 -  ] 
   22.17 -];
   22.18 +    ("haskell", (5, ":"))];
   22.19  
   22.20  end;
   22.21  *}
   22.22 @@ -2705,6 +2703,6 @@
   22.23  
   22.24  setup list_codegen_setup
   22.25  
   22.26 -setup "[CodegenPackage.rename_inconsistent]"
   22.27 +setup CodegenPackage.rename_inconsistent
   22.28  
   22.29  end
    23.1 --- a/src/HOL/Product_Type.thy	Thu Jan 19 15:45:10 2006 +0100
    23.2 +++ b/src/HOL/Product_Type.thy	Thu Jan 19 21:22:08 2006 +0100
    23.3 @@ -885,14 +885,13 @@
    23.4  
    23.5  in
    23.6  
    23.7 -val prod_codegen_setup = [
    23.8 -  Codegen.add_codegen "let_codegen" let_codegen,
    23.9 -  Codegen.add_codegen "split_codegen" split_codegen,
   23.10 +val prod_codegen_setup =
   23.11 +  Codegen.add_codegen "let_codegen" let_codegen #>
   23.12 +  Codegen.add_codegen "split_codegen" split_codegen #>
   23.13    CodegenPackage.add_appconst
   23.14 -    ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs)),
   23.15 +    ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs)) #>
   23.16    CodegenPackage.add_appconst
   23.17 -    ("split", ((1, 1), CodegenPackage.appgen_split strip_abs))
   23.18 -];
   23.19 +    ("split", ((1, 1), CodegenPackage.appgen_split strip_abs));
   23.20  
   23.21  end;
   23.22  *}
    24.1 --- a/src/HOL/Real/rat_arith.ML	Thu Jan 19 15:45:10 2006 +0100
    24.2 +++ b/src/HOL/Real/rat_arith.ML	Thu Jan 19 21:22:08 2006 +0100
    24.3 @@ -38,17 +38,16 @@
    24.4  val ratT = Type("Rational.rat", []);
    24.5  
    24.6  val rat_arith_setup =
    24.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD,
    24.8 - neqE, simpset} =>
    24.9 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   24.10     {add_mono_thms = add_mono_thms,
   24.11      mult_mono_thms = mult_mono_thms,
   24.12      inj_thms = int_inj_thms @ inj_thms,
   24.13      lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
   24.14      neqE =  neqE,
   24.15      simpset = simpset addsimps simps
   24.16 -                      addsimprocs simprocs}),
   24.17 -  arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT),
   24.18 -  arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT),
   24.19 -  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy)];
   24.20 +                      addsimprocs simprocs}) #>
   24.21 +  arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT) #>
   24.22 +  arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT) #>
   24.23 +  (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy));
   24.24  
   24.25  end;
    25.1 --- a/src/HOL/Real/real_arith.ML	Thu Jan 19 15:45:10 2006 +0100
    25.2 +++ b/src/HOL/Real/real_arith.ML	Thu Jan 19 21:22:08 2006 +0100
    25.3 @@ -118,16 +118,16 @@
    25.4    Fast_Arith.lin_arith_prover;
    25.5  
    25.6  val real_arith_setup =
    25.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    25.8 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    25.9     {add_mono_thms = add_mono_thms,
   25.10      mult_mono_thms = mult_mono_thms,
   25.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
   25.12      lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
   25.13      neqE = neqE,
   25.14 -    simpset = simpset addsimps simps}),
   25.15 -  arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
   25.16 -  arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
   25.17 -  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)];
   25.18 +    simpset = simpset addsimps simps}) #>
   25.19 +  arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
   25.20 +  arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT) #>
   25.21 +  (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy));
   25.22  
   25.23  (* some thms for injection nat => real:
   25.24  real_of_nat_zero
    26.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jan 19 15:45:10 2006 +0100
    26.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Jan 19 21:22:08 2006 +0100
    26.3 @@ -14,7 +14,7 @@
    26.4  sig
    26.5   val presburger_tac : bool -> bool -> int -> tactic
    26.6   val presburger_method : bool -> bool -> int -> Proof.method
    26.7 - val setup : (theory -> theory) list
    26.8 + val setup : theory -> theory
    26.9   val trace : bool ref
   26.10  end;
   26.11  
   26.12 @@ -364,12 +364,12 @@
   26.13    Method.insert_tac facts 1 THEN presburger_tac q a i)
   26.14  
   26.15  val setup =
   26.16 -  [Method.add_method ("presburger",
   26.17 -     presburger_args presburger_method,
   26.18 -     "decision procedure for Presburger arithmetic"),
   26.19 -   ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
   26.20 -     {splits = splits, inj_consts = inj_consts, discrete = discrete,
   26.21 -      presburger = SOME (presburger_tac true true)})];
   26.22 +  Method.add_method ("presburger",
   26.23 +    presburger_args presburger_method,
   26.24 +    "decision procedure for Presburger arithmetic") #>
   26.25 +  ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
   26.26 +    {splits = splits, inj_consts = inj_consts, discrete = discrete,
   26.27 +      presburger = SOME (presburger_tac true true)});
   26.28  
   26.29  end;
   26.30  
    27.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Jan 19 15:45:10 2006 +0100
    27.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Jan 19 21:22:08 2006 +0100
    27.3 @@ -7,7 +7,7 @@
    27.4  
    27.5  signature DATATYPE_CODEGEN =
    27.6  sig
    27.7 -  val setup: (theory -> theory) list
    27.8 +  val setup: theory -> theory
    27.9  end;
   27.10  
   27.11  structure DatatypeCodegen : DATATYPE_CODEGEN =
   27.12 @@ -297,18 +297,17 @@
   27.13    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   27.14  
   27.15  
   27.16 -val setup = [
   27.17 -  add_codegen "datatype" datatype_codegen,
   27.18 -  add_tycodegen "datatype" datatype_tycodegen,
   27.19 +val setup =
   27.20 +  add_codegen "datatype" datatype_codegen #>
   27.21 +  add_tycodegen "datatype" datatype_tycodegen #>
   27.22    CodegenPackage.set_is_datatype
   27.23 -    DatatypePackage.is_datatype,
   27.24 +    DatatypePackage.is_datatype #>
   27.25    CodegenPackage.set_get_all_datatype_cons
   27.26 -    DatatypePackage.get_all_datatype_cons,
   27.27 +    DatatypePackage.get_all_datatype_cons #>
   27.28    CodegenPackage.add_defgen
   27.29 -    ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons),
   27.30 +    ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons) #>
   27.31    CodegenPackage.ensure_datatype_case_consts
   27.32      DatatypePackage.get_datatype_case_consts
   27.33 -    DatatypePackage.get_case_const_data
   27.34 -];
   27.35 +    DatatypePackage.get_case_const_data;
   27.36  
   27.37  end;
    28.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Jan 19 15:45:10 2006 +0100
    28.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Jan 19 21:22:08 2006 +0100
    28.3 @@ -75,7 +75,7 @@
    28.4    val constrs_of : theory -> string -> term list option
    28.5    val case_const_of : theory -> string -> term option
    28.6    val weak_case_congs_of : theory -> thm list
    28.7 -  val setup: (theory -> theory) list
    28.8 +  val setup: theory -> theory
    28.9  end;
   28.10  
   28.11  structure DatatypePackage : DATATYPE_PACKAGE =
   28.12 @@ -433,8 +433,8 @@
   28.13  val dist_ss = HOL_ss addsimprocs [distinct_simproc];
   28.14  
   28.15  val simproc_setup =
   28.16 -  [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
   28.17 -   fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy)];
   28.18 +  Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #>
   28.19 +  (fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy));
   28.20  
   28.21  
   28.22  (**** translation rules for case ****)
   28.23 @@ -545,7 +545,7 @@
   28.24      (NameSpace.accesses' case_name)) (descr ~~ case_names));
   28.25  
   28.26  val trfun_setup =
   28.27 -  [Theory.add_advanced_trfuns ([], [("_case_syntax", case_tr)], [], [])];
   28.28 +  Theory.add_advanced_trfuns ([], [("_case_syntax", case_tr)], [], []);
   28.29  
   28.30  
   28.31  (* prepare types *)
   28.32 @@ -1019,7 +1019,8 @@
   28.33  
   28.34  (* setup theory *)
   28.35  
   28.36 -val setup = [DatatypesData.init, Method.add_methods tactic_emulations] @ simproc_setup @ trfun_setup;
   28.37 +val setup =
   28.38 +  DatatypesData.init #> Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
   28.39  
   28.40  
   28.41  (* outer syntax *)
    29.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jan 19 15:45:10 2006 +0100
    29.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jan 19 21:22:08 2006 +0100
    29.3 @@ -8,7 +8,7 @@
    29.4  signature INDUCTIVE_CODEGEN =
    29.5  sig
    29.6    val add : string option -> theory attribute
    29.7 -  val setup : (theory -> theory) list
    29.8 +  val setup : theory -> theory
    29.9  end;
   29.10  
   29.11  structure InductiveCodegen : INDUCTIVE_CODEGEN =
   29.12 @@ -732,10 +732,9 @@
   29.13      | _ => NONE);
   29.14  
   29.15  val setup =
   29.16 -  [add_codegen "inductive" inductive_codegen,
   29.17 -   CodegenData.init,
   29.18 -   add_attribute "ind"
   29.19 -     (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
   29.20 +  add_codegen "inductive" inductive_codegen #>
   29.21 +  CodegenData.init #>
   29.22 +  add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
   29.23  
   29.24  end;
   29.25  
    30.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jan 19 15:45:10 2006 +0100
    30.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 19 21:22:08 2006 +0100
    30.3 @@ -55,7 +55,7 @@
    30.4      theory -> theory *
    30.5        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    30.6         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    30.7 -  val setup: (theory -> theory) list
    30.8 +  val setup: theory -> theory
    30.9  end;
   30.10  
   30.11  structure InductivePackage: INDUCTIVE_PACKAGE =
   30.12 @@ -868,10 +868,10 @@
   30.13  (* setup theory *)
   30.14  
   30.15  val setup =
   30.16 - [InductiveData.init,
   30.17 +  InductiveData.init #>
   30.18    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   30.19 -    "dynamic case analysis on sets")],
   30.20 -  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
   30.21 +    "dynamic case analysis on sets")] #>
   30.22 +  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
   30.23  
   30.24  
   30.25  (* outer syntax *)
    31.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jan 19 15:45:10 2006 +0100
    31.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jan 19 21:22:08 2006 +0100
    31.3 @@ -9,7 +9,7 @@
    31.4  signature INDUCTIVE_REALIZER =
    31.5  sig
    31.6    val add_ind_realizers: string -> string list -> theory -> theory
    31.7 -  val setup: (theory -> theory) list
    31.8 +  val setup: theory -> theory
    31.9  end;
   31.10  
   31.11  structure InductiveRealizer : INDUCTIVE_REALIZER =
   31.12 @@ -487,9 +487,10 @@
   31.13      Scan.option (Scan.lift (Args.colon) |--
   31.14        Scan.repeat1 Args.global_const))) >> rlz_attrib);
   31.15  
   31.16 -val setup = [Attrib.add_attributes [("ind_realizer",
   31.17 -  (rlz_attrib_global, K Attrib.undef_local_attribute),
   31.18 -  "add realizers for inductive set")]];
   31.19 +val setup =
   31.20 +  Attrib.add_attributes [("ind_realizer",
   31.21 +    (rlz_attrib_global, K Attrib.undef_local_attribute),
   31.22 +    "add realizers for inductive set")];
   31.23  
   31.24  end;
   31.25  
    32.1 --- a/src/HOL/Tools/meson.ML	Thu Jan 19 15:45:10 2006 +0100
    32.2 +++ b/src/HOL/Tools/meson.ML	Thu Jan 19 21:22:08 2006 +0100
    32.3 @@ -590,11 +590,11 @@
    32.4  val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
    32.5  
    32.6  val skolemize_setup =
    32.7 - [Method.add_methods
    32.8 -  [("skolemize", Method.no_args skolemize_meth, 
    32.9 -    "Skolemization into existential quantifiers"),
   32.10 -   ("make_clauses", Method.no_args make_clauses_meth, 
   32.11 -    "Conversion to !!-quantified meta-level clauses")]];
   32.12 +  Method.add_methods
   32.13 +    [("skolemize", Method.no_args skolemize_meth, 
   32.14 +      "Skolemization into existential quantifiers"),
   32.15 +     ("make_clauses", Method.no_args make_clauses_meth, 
   32.16 +      "Conversion to !!-quantified meta-level clauses")];
   32.17  
   32.18  end;
   32.19  
    33.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Jan 19 15:45:10 2006 +0100
    33.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jan 19 21:22:08 2006 +0100
    33.3 @@ -8,7 +8,7 @@
    33.4  
    33.5  signature NUMERAL_SYNTAX =
    33.6  sig
    33.7 -  val setup: (theory -> theory) list
    33.8 +  val setup: theory -> theory
    33.9  end;
   33.10  
   33.11  structure NumeralSyntax: NUMERAL_SYNTAX =
   33.12 @@ -55,9 +55,9 @@
   33.13  (* theory setup *)
   33.14  
   33.15  val setup =
   33.16 - [Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"],
   33.17 -  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"],
   33.18 -   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
   33.19 -  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
   33.20 +  Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #>
   33.21 +  Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #>
   33.22 +  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
   33.23 +  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
   33.24  
   33.25  end;
    34.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Jan 19 15:45:10 2006 +0100
    34.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Jan 19 21:22:08 2006 +0100
    34.3 @@ -29,7 +29,7 @@
    34.4    val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state
    34.5    val recdef_tc_i: bstring * theory attribute list -> string -> int option
    34.6      -> theory -> Proof.state
    34.7 -  val setup: (theory -> theory) list
    34.8 +  val setup: theory -> theory
    34.9  end;
   34.10  
   34.11  structure RecdefPackage: RECDEF_PACKAGE =
   34.12 @@ -294,14 +294,15 @@
   34.13  (* setup theory *)
   34.14  
   34.15  val setup =
   34.16 - [GlobalRecdefData.init, LocalRecdefData.init,
   34.17 +  GlobalRecdefData.init #>
   34.18 +  LocalRecdefData.init #>
   34.19    Attrib.add_attributes
   34.20     [(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
   34.21        "declaration of recdef simp rule"),
   34.22      (recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
   34.23        "declaration of recdef cong rule"),
   34.24      (recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
   34.25 -      "declaration of recdef wf rule")]];
   34.26 +      "declaration of recdef wf rule")];
   34.27  
   34.28  
   34.29  (* outer syntax *)
    35.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu Jan 19 15:45:10 2006 +0100
    35.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu Jan 19 21:22:08 2006 +0100
    35.3 @@ -11,7 +11,7 @@
    35.4    val del: theory attribute
    35.5    val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
    35.6    val get_thm_equations: theory -> string * typ -> (thm list * typ) option
    35.7 -  val setup: (theory -> theory) list
    35.8 +  val setup: theory -> theory
    35.9  end;
   35.10  
   35.11  structure RecfunCodegen : RECFUN_CODEGEN =
   35.12 @@ -191,14 +191,13 @@
   35.13    | _ => NONE);
   35.14  
   35.15  
   35.16 -val setup = [
   35.17 -  CodegenData.init,
   35.18 -  add_codegen "recfun" recfun_codegen,
   35.19 +val setup =
   35.20 +  CodegenData.init #>
   35.21 +  add_codegen "recfun" recfun_codegen #>
   35.22    add_attribute ""
   35.23      (   Args.del |-- Scan.succeed del
   35.24 -     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
   35.25 +     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add) #>
   35.26    CodegenPackage.add_eqextr
   35.27 -    ("rec", fn thy => fn _ => get_thm_equations thy)
   35.28 -];
   35.29 +    ("rec", fn thy => fn _ => get_thm_equations thy);
   35.30  
   35.31  end;
    36.1 --- a/src/HOL/Tools/reconstruction.ML	Thu Jan 19 15:45:10 2006 +0100
    36.2 +++ b/src/HOL/Tools/reconstruction.ML	Thu Jan 19 21:22:08 2006 +0100
    36.3 @@ -132,12 +132,12 @@
    36.4  (** theory setup **)
    36.5  
    36.6  val setup =
    36.7 -  [Attrib.add_attributes
    36.8 -     [("binary", (binary_global, binary_local), "binary resolution"),
    36.9 -      ("paramod", (paramod_global, paramod_local), "paramodulation"),
   36.10 -      ("demod", (demod_global, demod_local), "demodulation"),
   36.11 -      ("factor", (factor, factor), "factoring"),
   36.12 -      ("clausify", (clausify, clausify), "conversion to clauses")]];
   36.13 +  Attrib.add_attributes
   36.14 +    [("binary", (binary_global, binary_local), "binary resolution"),
   36.15 +     ("paramod", (paramod_global, paramod_local), "paramodulation"),
   36.16 +     ("demod", (demod_global, demod_local), "demodulation"),
   36.17 +     ("factor", (factor, factor), "factoring"),
   36.18 +     ("clausify", (clausify, clausify), "conversion to clauses")];
   36.19  
   36.20  end
   36.21  end
    37.1 --- a/src/HOL/Tools/record_package.ML	Thu Jan 19 15:45:10 2006 +0100
    37.2 +++ b/src/HOL/Tools/record_package.ML	Thu Jan 19 21:22:08 2006 +0100
    37.3 @@ -39,7 +39,7 @@
    37.4      -> theory -> theory
    37.5    val add_record_i: string list * string -> (typ list * string) option
    37.6      -> (string * typ * mixfix) list -> theory -> theory
    37.7 -  val setup: (theory -> theory) list
    37.8 +  val setup: theory -> theory
    37.9  end;
   37.10  
   37.11  
   37.12 @@ -2098,11 +2098,11 @@
   37.13  (* setup theory *)
   37.14  
   37.15  val setup =
   37.16 - [RecordsData.init,
   37.17 -  Theory.add_trfuns ([], parse_translation, [], []),
   37.18 -  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
   37.19 +  RecordsData.init #>
   37.20 +  Theory.add_trfuns ([], parse_translation, [], []) #>
   37.21 +  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
   37.22    (fn thy => (Simplifier.change_simpset_of thy
   37.23 -    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy))];
   37.24 +    (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy));
   37.25  
   37.26  (* outer syntax *)
   37.27  
    38.1 --- a/src/HOL/Tools/refute.ML	Thu Jan 19 15:45:10 2006 +0100
    38.2 +++ b/src/HOL/Tools/refute.ML	Thu Jan 19 21:22:08 2006 +0100
    38.3 @@ -50,7 +50,7 @@
    38.4  	val refute_term    : theory -> (string * string) list -> Term.term -> unit  (* tries to find a model that refutes a formula *)
    38.5  	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    38.6  
    38.7 -	val setup : (theory -> theory) list
    38.8 +	val setup : theory -> theory
    38.9  end;
   38.10  
   38.11  structure Refute : REFUTE =
   38.12 @@ -2605,25 +2605,25 @@
   38.13  	(* (theory -> theory) list *)
   38.14  
   38.15  	val setup =
   38.16 -		[RefuteData.init,
   38.17 -		 add_interpreter "stlc"    stlc_interpreter,
   38.18 -		 add_interpreter "Pure"    Pure_interpreter,
   38.19 -		 add_interpreter "HOLogic" HOLogic_interpreter,
   38.20 -		 add_interpreter "set"     set_interpreter,
   38.21 -		 add_interpreter "IDT"             IDT_interpreter,
   38.22 -		 add_interpreter "IDT_constructor" IDT_constructor_interpreter,
   38.23 -		 add_interpreter "IDT_recursion"   IDT_recursion_interpreter,
   38.24 -		 add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter,
   38.25 -		 add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter,
   38.26 -		 add_interpreter "Nat.op <" Nat_less_interpreter,
   38.27 -		 add_interpreter "Nat.op +" Nat_plus_interpreter,
   38.28 -		 add_interpreter "Nat.op -" Nat_minus_interpreter,
   38.29 -		 add_interpreter "Nat.op *" Nat_mult_interpreter,
   38.30 -		 add_interpreter "List.op @" List_append_interpreter,
   38.31 -		 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter,
   38.32 -		 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter,
   38.33 -		 add_printer "stlc" stlc_printer,
   38.34 -		 add_printer "set"  set_printer,
   38.35 -		 add_printer "IDT"  IDT_printer];
   38.36 +		 RefuteData.init #>
   38.37 +		 add_interpreter "stlc"    stlc_interpreter #>
   38.38 +		 add_interpreter "Pure"    Pure_interpreter #>
   38.39 +		 add_interpreter "HOLogic" HOLogic_interpreter #>
   38.40 +		 add_interpreter "set"     set_interpreter #>
   38.41 +		 add_interpreter "IDT"             IDT_interpreter #>
   38.42 +		 add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
   38.43 +		 add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
   38.44 +		 add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
   38.45 +		 add_interpreter "Finite_Set.Finites" Finite_Set_Finites_interpreter #>
   38.46 +		 add_interpreter "Nat.op <" Nat_less_interpreter #>
   38.47 +		 add_interpreter "Nat.op +" Nat_plus_interpreter #>
   38.48 +		 add_interpreter "Nat.op -" Nat_minus_interpreter #>
   38.49 +		 add_interpreter "Nat.op *" Nat_mult_interpreter #>
   38.50 +		 add_interpreter "List.op @" List_append_interpreter #>
   38.51 +		 add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
   38.52 +		 add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
   38.53 +		 add_printer "stlc" stlc_printer #>
   38.54 +		 add_printer "set"  set_printer #>
   38.55 +		 add_printer "IDT"  IDT_printer;
   38.56  
   38.57  end
    39.1 --- a/src/HOL/Tools/res_atp_methods.ML	Thu Jan 19 15:45:10 2006 +0100
    39.2 +++ b/src/HOL/Tools/res_atp_methods.ML	Thu Jan 19 21:22:08 2006 +0100
    39.3 @@ -46,16 +46,13 @@
    39.4  
    39.5  val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time);
    39.6  
    39.7 -val ResAtps_setup = [Method.add_methods 
    39.8 -		 [("vampireF", ResAtpSetup.atp_method vampireF_tac, "A Vampire method for FOL problems"),
    39.9 -		   ("eproverF", ResAtpSetup.atp_method eproverF_tac, "A E prover method for FOL problems"),
   39.10 -			("vampireH",ResAtpSetup.atp_method vampireH_tac, "A Vampire method for HOL problems"),
   39.11 -				("eproverH",ResAtpSetup.atp_method eproverH_tac,"A E prover method for HOL problems"),
   39.12 -				("eprover",ResAtpSetup.atp_method eprover_tac,"A E prover method for FOL and HOL problems"),
   39.13 -				("vampire",ResAtpSetup.atp_method vampire_tac,"A Vampire method for FOL and HOL problems")
   39.14 -]];
   39.15 -
   39.16 -
   39.17 -
   39.18 +val ResAtps_setup =
   39.19 +  Method.add_methods 
   39.20 +    [("vampireF", ResAtpSetup.atp_method vampireF_tac, "Vampire for FOL problems"),
   39.21 +     ("eproverF", ResAtpSetup.atp_method eproverF_tac, "E prover for FOL problems"),
   39.22 +     ("vampireH", ResAtpSetup.atp_method vampireH_tac, "Vampire for HOL problems"),
   39.23 +     ("eproverH", ResAtpSetup.atp_method eproverH_tac, "E prover for HOL problems"),
   39.24 +     ("eprover", ResAtpSetup.atp_method eprover_tac, "E prover for FOL and HOL problems"),
   39.25 +     ("vampire", ResAtpSetup.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
   39.26  
   39.27  end
    40.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Jan 19 15:45:10 2006 +0100
    40.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Jan 19 21:22:08 2006 +0100
    40.3 @@ -27,8 +27,8 @@
    40.4    val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
    40.5    val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
    40.6  
    40.7 -  val meson_method_setup : (theory -> theory) list  (*Reconstruction.thy*)
    40.8 -  val setup : (theory -> theory) list               (*Main.thy*)
    40.9 +  val meson_method_setup : theory -> theory
   40.10 +  val setup : theory -> theory
   40.11    end;
   40.12  
   40.13  structure ResAxioms : RES_AXIOMS =
   40.14 @@ -471,9 +471,9 @@
   40.15      (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
   40.16  
   40.17  val meson_method_setup =
   40.18 - [Method.add_methods
   40.19 -  [("meson", Method.thms_ctxt_args meson_meth, 
   40.20 -    "The MESON resolution proof procedure")]];
   40.21 +  Method.add_methods
   40.22 +    [("meson", Method.thms_ctxt_args meson_meth, 
   40.23 +      "The MESON resolution proof procedure")];
   40.24  
   40.25  
   40.26  
   40.27 @@ -497,6 +497,6 @@
   40.28   [("skolem", (skolem_global, skolem_local),
   40.29      "skolemization of a theorem")];
   40.30  
   40.31 -val setup = [clause_cache_setup, setup_attrs];
   40.32 +val setup = clause_cache_setup #> setup_attrs;
   40.33  
   40.34  end; 
    41.1 --- a/src/HOL/Tools/split_rule.ML	Thu Jan 19 15:45:10 2006 +0100
    41.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Jan 19 21:22:08 2006 +0100
    41.3 @@ -16,7 +16,7 @@
    41.4    include BASIC_SPLIT_RULE
    41.5    val split_rule_var: term * thm -> thm
    41.6    val split_rule_goal: string list list -> thm -> thm
    41.7 -  val setup: (theory -> theory) list
    41.8 +  val setup: theory -> theory
    41.9  end;
   41.10  
   41.11  structure SplitRule: SPLIT_RULE =
   41.12 @@ -141,9 +141,9 @@
   41.13      >> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
   41.14  
   41.15  val setup =
   41.16 - [Attrib.add_attributes
   41.17 -  [("split_format", (split_format, split_format),
   41.18 -    "split pair-typed subterms in premises, or function arguments")]];
   41.19 +  Attrib.add_attributes
   41.20 +    [("split_format", (split_format, split_format),
   41.21 +      "split pair-typed subterms in premises, or function arguments")];
   41.22  
   41.23  end;
   41.24  
    42.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Jan 19 15:45:10 2006 +0100
    42.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Jan 19 21:22:08 2006 +0100
    42.3 @@ -23,7 +23,7 @@
    42.4      * (string * string) option -> theory -> Proof.state
    42.5    val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    42.6      * (string * string) option -> theory -> Proof.state
    42.7 -  val setup: (theory -> theory) list
    42.8 +  val setup: theory -> theory
    42.9  end;
   42.10  
   42.11  structure TypedefPackage: TYPEDEF_PACKAGE =
   42.12 @@ -360,9 +360,9 @@
   42.13    | typedef_tycodegen thy defs gr dep module brack _ = NONE;
   42.14  
   42.15  val setup =
   42.16 -  [TypedefData.init,
   42.17 -   Codegen.add_codegen "typedef" typedef_codegen,
   42.18 -   Codegen.add_tycodegen "typedef" typedef_tycodegen];
   42.19 +  TypedefData.init #>
   42.20 +  Codegen.add_codegen "typedef" typedef_codegen #>
   42.21 +  Codegen.add_tycodegen "typedef" typedef_tycodegen;
   42.22  
   42.23  
   42.24  
    43.1 --- a/src/HOL/antisym_setup.ML	Thu Jan 19 15:45:10 2006 +0100
    43.2 +++ b/src/HOL/antisym_setup.ML	Thu Jan 19 21:22:08 2006 +0100
    43.3 @@ -48,7 +48,7 @@
    43.4  in
    43.5  
    43.6  val antisym_setup =
    43.7 - [fn thy => (Simplifier.change_simpset_of thy
    43.8 -  (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy)]
    43.9 + (fn thy => (Simplifier.change_simpset_of thy
   43.10 +  (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy));
   43.11  
   43.12  end
    44.1 --- a/src/HOL/arith_data.ML	Thu Jan 19 15:45:10 2006 +0100
    44.2 +++ b/src/HOL/arith_data.ML	Thu Jan 19 21:22:08 2006 +0100
    44.3 @@ -420,8 +420,8 @@
    44.4  in
    44.5  
    44.6  val init_lin_arith_data =
    44.7 - Fast_Arith.setup @
    44.8 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    44.9 + Fast_Arith.setup #>
   44.10 + Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   44.11     {add_mono_thms = add_mono_thms @
   44.12      add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
   44.13      mult_mono_thms = mult_mono_thms,
   44.14 @@ -433,8 +433,9 @@
   44.15                     addsimprocs [ab_group_add_cancel.sum_conv,
   44.16                                  ab_group_add_cancel.rel_conv]
   44.17                     (*abel_cancel helps it work in abstract algebraic domains*)
   44.18 -                   addsimprocs nat_cancel_sums_add}),
   44.19 -  ArithTheoryData.init, arith_discrete "nat"];
   44.20 +                   addsimprocs nat_cancel_sums_add}) #>
   44.21 +  ArithTheoryData.init #>
   44.22 +  arith_discrete "nat";
   44.23  
   44.24  end;
   44.25  
   44.26 @@ -576,14 +577,14 @@
   44.27  (* theory setup *)
   44.28  
   44.29  val arith_setup =
   44.30 -  init_lin_arith_data @
   44.31 -  [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
   44.32 +  init_lin_arith_data #>
   44.33 +  (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
   44.34      addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
   44.35 -    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy),
   44.36 +    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #>
   44.37    Method.add_methods
   44.38      [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
   44.39 -      "decide linear arithmethic")],
   44.40 +      "decide linear arithmethic")] #>
   44.41    Attrib.add_attributes [("arith_split",
   44.42      (Attrib.no_args arith_split_add,
   44.43       Attrib.no_args Attrib.undef_local_attribute),
   44.44 -    "declaration of split rules for arithmetic procedure")]];
   44.45 +    "declaration of split rules for arithmetic procedure")];
    45.1 --- a/src/HOL/cladata.ML	Thu Jan 19 15:45:10 2006 +0100
    45.2 +++ b/src/HOL/cladata.ML	Thu Jan 19 21:22:08 2006 +0100
    45.3 @@ -62,4 +62,4 @@
    45.4  val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality] 
    45.5                       addSEs [exE] addEs [allE];
    45.6  
    45.7 -val clasetup = [fn thy => (change_claset_of thy (fn _ => HOL_cs); thy)];
    45.8 +val clasetup = (fn thy => (change_claset_of thy (fn _ => HOL_cs); thy));
    46.1 --- a/src/HOL/simpdata.ML	Thu Jan 19 15:45:10 2006 +0100
    46.2 +++ b/src/HOL/simpdata.ML	Thu Jan 19 21:22:08 2006 +0100
    46.3 @@ -425,7 +425,7 @@
    46.4  
    46.5  (* default simpset *)
    46.6  val simpsetup =
    46.7 -  [fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)];
    46.8 +  (fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy));
    46.9  
   46.10  
   46.11  (*** integration of simplifier with classical reasoner ***)
    47.1 --- a/src/HOLCF/cont_proc.ML	Thu Jan 19 15:45:10 2006 +0100
    47.2 +++ b/src/HOLCF/cont_proc.ML	Thu Jan 19 21:22:08 2006 +0100
    47.3 @@ -10,7 +10,7 @@
    47.4    val all_cont_thms: term -> thm list
    47.5    val cont_tac: int -> tactic
    47.6    val cont_proc: theory -> simproc
    47.7 -  val setup: (theory -> theory) list
    47.8 +  val setup: theory -> theory
    47.9  end;
   47.10  
   47.11  structure ContProc: CONT_PROC =
   47.12 @@ -110,6 +110,6 @@
   47.13  end;
   47.14  
   47.15  val setup =
   47.16 -  [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [cont_proc thy]); thy)];
   47.17 +  (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [cont_proc thy]); thy));
   47.18  
   47.19  end;
    48.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jan 19 15:45:10 2006 +0100
    48.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jan 19 21:22:08 2006 +0100
    48.3 @@ -70,7 +70,7 @@
    48.4  
    48.5  signature FAST_LIN_ARITH =
    48.6  sig
    48.7 -  val setup: (theory -> theory) list
    48.8 +  val setup: theory -> theory
    48.9    val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   48.10                   lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
   48.11                   -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   48.12 @@ -119,7 +119,7 @@
   48.13  end);
   48.14  
   48.15  val map_data = Data.map;
   48.16 -val setup = [Data.init];
   48.17 +val setup = Data.init;
   48.18  
   48.19  
   48.20  
    49.1 --- a/src/Provers/blast.ML	Thu Jan 19 15:45:10 2006 +0100
    49.2 +++ b/src/Provers/blast.ML	Thu Jan 19 21:22:08 2006 +0100
    49.3 @@ -79,7 +79,7 @@
    49.4    val depth_limit : int ref
    49.5    val blast_tac         : claset -> int -> tactic
    49.6    val Blast_tac         : int -> tactic
    49.7 -  val setup             : (theory -> theory) list
    49.8 +  val setup             : theory -> theory
    49.9    (*debugging tools*)
   49.10    val stats             : bool ref
   49.11    val trace             : bool ref
   49.12 @@ -1329,7 +1329,7 @@
   49.13    | blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
   49.14  
   49.15  val setup =
   49.16 - [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
   49.17 +  Method.add_methods [("blast", blast_args blast_meth, "tableau prover")];
   49.18  
   49.19  
   49.20  end;
    50.1 --- a/src/Provers/clasimp.ML	Thu Jan 19 15:45:10 2006 +0100
    50.2 +++ b/src/Provers/clasimp.ML	Thu Jan 19 21:22:08 2006 +0100
    50.3 @@ -64,7 +64,7 @@
    50.4    val iff_del: Context.generic attribute
    50.5    val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    50.6    val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    50.7 -  val setup: (theory -> theory) list
    50.8 +  val setup: theory -> theory
    50.9  end;
   50.10  
   50.11  functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
   50.12 @@ -327,14 +327,14 @@
   50.13  (* theory setup *)
   50.14  
   50.15  val setup =
   50.16 - [Attrib.add_attributes
   50.17 -  [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")],
   50.18 + (Attrib.add_attributes
   50.19 +   [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")] #>
   50.20    Method.add_methods
   50.21     [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
   50.22      ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
   50.23      ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
   50.24      ("force", clasimp_method' force_tac, "force"),
   50.25      ("auto", auto_args auto_meth, "auto"),
   50.26 -    ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]];
   50.27 +    ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]);
   50.28  
   50.29  end;
    51.1 --- a/src/Provers/classical.ML	Thu Jan 19 15:45:10 2006 +0100
    51.2 +++ b/src/Provers/classical.ML	Thu Jan 19 21:22:08 2006 +0100
    51.3 @@ -155,7 +155,7 @@
    51.4    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    51.5    val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
    51.6    val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
    51.7 -  val setup: (theory -> theory) list
    51.8 +  val setup: theory -> theory
    51.9  end;
   51.10  
   51.11  
   51.12 @@ -1080,7 +1080,7 @@
   51.13  
   51.14  (** theory setup **)
   51.15  
   51.16 -val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
   51.17 +val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
   51.18  
   51.19  
   51.20  
    52.1 --- a/src/Provers/eqsubst.ML	Thu Jan 19 15:45:10 2006 +0100
    52.2 +++ b/src/Provers/eqsubst.ML	Thu Jan 19 21:22:08 2006 +0100
    52.3 @@ -7,7 +7,7 @@
    52.4  
    52.5  signature EQSUBST =
    52.6  sig
    52.7 -  val setup : (Theory.theory -> Theory.theory) list
    52.8 +  val setup : theory -> theory
    52.9  end;
   52.10  
   52.11  structure EqSubst: EQSUBST =
   52.12 @@ -337,6 +337,6 @@
   52.13  
   52.14  
   52.15  val setup =
   52.16 -  [Method.add_method ("subst", subst_meth, "substiution with an equation")];
   52.17 +  Method.add_method ("subst", subst_meth, "substiution with an equation");
   52.18  
   52.19  end;
    53.1 --- a/src/Provers/hypsubst.ML	Thu Jan 19 15:45:10 2006 +0100
    53.2 +++ b/src/Provers/hypsubst.ML	Thu Jan 19 21:22:08 2006 +0100
    53.3 @@ -58,7 +58,7 @@
    53.4    val inspect_pair           : bool -> bool -> term * term * typ -> bool
    53.5    val mk_eqs                 : bool -> thm -> thm list
    53.6    val stac		     : thm -> int -> tactic
    53.7 -  val hypsubst_setup         : (theory -> theory) list
    53.8 +  val hypsubst_setup         : theory -> theory
    53.9    end;
   53.10  
   53.11  
   53.12 @@ -242,8 +242,8 @@
   53.13  (* theory setup *)
   53.14  
   53.15  val hypsubst_setup =
   53.16 - [Method.add_methods
   53.17 -  [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
   53.18 -   ("simplesubst", subst_meth, "simple substitution")]];
   53.19 +  Method.add_methods
   53.20 +    [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
   53.21 +     ("simplesubst", subst_meth, "simple substitution")];
   53.22  
   53.23  end;
    54.1 --- a/src/Provers/induct_method.ML	Thu Jan 19 15:45:10 2006 +0100
    54.2 +++ b/src/Provers/induct_method.ML	Thu Jan 19 21:22:08 2006 +0100
    54.3 @@ -32,7 +32,7 @@
    54.4      cases_tactic
    54.5    val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
    54.6      thm option -> thm list -> int -> cases_tactic
    54.7 -  val setup: (theory -> theory) list
    54.8 +  val setup: theory -> theory
    54.9  end;
   54.10  
   54.11  functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
   54.12 @@ -556,9 +556,9 @@
   54.13  (** theory setup **)
   54.14  
   54.15  val setup =
   54.16 -  [Method.add_methods
   54.17 +  Method.add_methods
   54.18      [(InductAttrib.casesN, cases_meth, "case analysis on types or sets"),
   54.19       (InductAttrib.inductN, induct_meth, "induction on types or sets"),
   54.20 -     (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")]];
   54.21 +     (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")];
   54.22  
   54.23  end;
    55.1 --- a/src/Provers/splitter.ML	Thu Jan 19 15:45:10 2006 +0100
    55.2 +++ b/src/Provers/splitter.ML	Thu Jan 19 21:22:08 2006 +0100
    55.3 @@ -35,7 +35,7 @@
    55.4    val split_add: Context.generic attribute
    55.5    val split_del: Context.generic attribute
    55.6    val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
    55.7 -  val setup: (theory -> theory) list
    55.8 +  val setup: theory -> theory
    55.9  end;
   55.10  
   55.11  functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
   55.12 @@ -455,9 +455,9 @@
   55.13  (* theory setup *)
   55.14  
   55.15  val setup =
   55.16 - [Attrib.add_attributes
   55.17 + (Attrib.add_attributes
   55.18    [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
   55.19 -    "declaration of case split rule")],
   55.20 -  Method.add_methods [(splitN, split_meth, "apply case split rule")]];
   55.21 +    "declaration of case split rule")] #>
   55.22 +  Method.add_methods [(splitN, split_meth, "apply case split rule")]);
   55.23  
   55.24  end;
    56.1 --- a/src/Pure/Isar/attrib.ML	Thu Jan 19 15:45:10 2006 +0100
    56.2 +++ b/src/Pure/Isar/attrib.ML	Thu Jan 19 21:22:08 2006 +0100
    56.3 @@ -114,7 +114,7 @@
    56.4      end;
    56.5  end);
    56.6  
    56.7 -val _ = Context.add_setup [AttributesData.init];
    56.8 +val _ = Context.add_setup AttributesData.init;
    56.9  val print_attributes = AttributesData.print;
   56.10  
   56.11  
   56.12 @@ -487,7 +487,7 @@
   56.13  (* theory setup *)
   56.14  
   56.15  val _ = Context.add_setup
   56.16 - [add_attributes
   56.17 + (add_attributes
   56.18     [("tagged", common tagged, "tagged theorem"),
   56.19      ("untagged", common untagged, "untagged theorem"),
   56.20      ("COMP", common COMP_att, "direct composition with rules (no lifting)"),
   56.21 @@ -511,7 +511,7 @@
   56.22      ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
   56.23        "declaration of rulify rule"),
   56.24      ("rule_format", common rule_format_att, "result put into standard rule format"),
   56.25 -    ("attribute", common internal_att, "internal attribute")]];
   56.26 +    ("attribute", common internal_att, "internal attribute")]);
   56.27  
   56.28  end;
   56.29  
    57.1 --- a/src/Pure/Isar/calculation.ML	Thu Jan 19 15:45:10 2006 +0100
    57.2 +++ b/src/Pure/Isar/calculation.ML	Thu Jan 19 21:22:08 2006 +0100
    57.3 @@ -46,7 +46,7 @@
    57.4      end;
    57.5  );
    57.6  
    57.7 -val _ = Context.add_setup [CalculationData.init];
    57.8 +val _ = Context.add_setup CalculationData.init;
    57.9  val print_rules = CalculationData.print;
   57.10  
   57.11  
   57.12 @@ -97,13 +97,13 @@
   57.13  val sym_att = Attrib.add_del_args sym_add sym_del;
   57.14  
   57.15  val _ = Context.add_setup
   57.16 - [Attrib.add_attributes
   57.17 + (Attrib.add_attributes
   57.18     [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
   57.19      ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
   57.20 -    ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")],
   57.21 -  snd o PureThy.add_thms
   57.22 +    ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")] #>
   57.23 +  PureThy.add_thms
   57.24     [(("", transitive_thm), [Attrib.theory trans_add]),
   57.25 -    (("", symmetric_thm), [Attrib.theory sym_add])]];
   57.26 +    (("", symmetric_thm), [Attrib.theory sym_add])] #> snd);
   57.27  
   57.28  
   57.29  
    58.1 --- a/src/Pure/Isar/context_rules.ML	Thu Jan 19 15:45:10 2006 +0100
    58.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Jan 19 21:22:08 2006 +0100
    58.3 @@ -123,7 +123,7 @@
    58.4      in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    58.5  );
    58.6  
    58.7 -val _ = Context.add_setup [Rules.init];
    58.8 +val _ = Context.add_setup Rules.init;
    58.9  val print_rules = Rules.print;
   58.10  
   58.11  
   58.12 @@ -203,7 +203,7 @@
   58.13  val dest_query  = rule_add elim_queryK Tactic.make_elim;
   58.14  
   58.15  val _ = Context.add_setup
   58.16 -  [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]];
   58.17 +  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]);
   58.18  
   58.19  
   58.20  (* concrete syntax *)
   58.21 @@ -222,6 +222,6 @@
   58.22    ("rule", Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
   58.23      "remove declaration of intro/elim/dest rule")];
   58.24  
   58.25 -val _ = Context.add_setup [Attrib.add_attributes rule_atts];
   58.26 +val _ = Context.add_setup (Attrib.add_attributes rule_atts);
   58.27  
   58.28  end;
    59.1 --- a/src/Pure/Isar/induct_attrib.ML	Thu Jan 19 15:45:10 2006 +0100
    59.2 +++ b/src/Pure/Isar/induct_attrib.ML	Thu Jan 19 21:22:08 2006 +0100
    59.3 @@ -134,7 +134,7 @@
    59.4      end
    59.5  );
    59.6  
    59.7 -val _ = Context.add_setup [Induct.init];
    59.8 +val _ = Context.add_setup Induct.init;
    59.9  val print_rules = Induct.print;
   59.10  val dest_rules = dest o Induct.get;
   59.11  
   59.12 @@ -224,9 +224,9 @@
   59.13  end;
   59.14  
   59.15  val _ = Context.add_setup
   59.16 - [Attrib.add_attributes
   59.17 + (Attrib.add_attributes
   59.18    [(casesN, Attrib.common cases_att, "declaration of cases rule for type or set"),
   59.19     (inductN, Attrib.common induct_att, "declaration of induction rule for type or set"),
   59.20 -   (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]];
   59.21 +   (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]);
   59.22  
   59.23  end;
    60.1 --- a/src/Pure/Isar/locale.ML	Thu Jan 19 15:45:10 2006 +0100
    60.2 +++ b/src/Pure/Isar/locale.ML	Thu Jan 19 21:22:08 2006 +0100
    60.3 @@ -278,7 +278,7 @@
    60.4      |> Pretty.writeln;
    60.5  end);
    60.6  
    60.7 -val _ = Context.add_setup [GlobalLocalesData.init];
    60.8 +val _ = Context.add_setup GlobalLocalesData.init;
    60.9  
   60.10  
   60.11  
   60.12 @@ -293,7 +293,7 @@
   60.13    fun print _ _ = ();
   60.14  end);
   60.15  
   60.16 -val _ = Context.add_setup [LocalLocalesData.init];
   60.17 +val _ = Context.add_setup LocalLocalesData.init;
   60.18  
   60.19  
   60.20  (* access locales *)
   60.21 @@ -1718,8 +1718,8 @@
   60.22  end;
   60.23  
   60.24  val _ = Context.add_setup
   60.25 - [add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]],
   60.26 -  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]];
   60.27 + (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #>
   60.28 +  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]);
   60.29  
   60.30  
   60.31  
    61.1 --- a/src/Pure/Isar/method.ML	Thu Jan 19 15:45:10 2006 +0100
    61.2 +++ b/src/Pure/Isar/method.ML	Thu Jan 19 21:22:08 2006 +0100
    61.3 @@ -544,7 +544,7 @@
    61.4      end;
    61.5  end);
    61.6  
    61.7 -val _ = Context.add_setup [MethodsData.init];
    61.8 +val _ = Context.add_setup MethodsData.init;
    61.9  val print_methods = MethodsData.print;
   61.10  
   61.11  
   61.12 @@ -721,9 +721,9 @@
   61.13  val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
   61.14  
   61.15  
   61.16 -(* pure_methods *)
   61.17 +(* theory setup *)
   61.18  
   61.19 -val pure_methods =
   61.20 +val _ = Context.add_setup (add_methods
   61.21   [("fail", no_args fail, "force failure"),
   61.22    ("succeed", no_args succeed, "succeed"),
   61.23    ("-", no_args insert_facts, "do nothing (insert current facts only)"),
   61.24 @@ -751,9 +751,7 @@
   61.25    ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
   61.26    ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
   61.27    ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
   61.28 -  ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
   61.29 -
   61.30 -val _ = Context.add_setup [add_methods pure_methods];
   61.31 +  ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);
   61.32  
   61.33  
   61.34  (*final declarations of this structure!*)
    62.1 --- a/src/Pure/Isar/object_logic.ML	Thu Jan 19 15:45:10 2006 +0100
    62.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Jan 19 21:22:08 2006 +0100
    62.3 @@ -56,7 +56,7 @@
    62.4    fun print _ _ = ();
    62.5  end);
    62.6  
    62.7 -val _ = Context.add_setup [ObjectLogicData.init];
    62.8 +val _ = Context.add_setup ObjectLogicData.init;
    62.9  
   62.10  
   62.11  
    63.1 --- a/src/Pure/Isar/proof_context.ML	Thu Jan 19 15:45:10 2006 +0100
    63.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Jan 19 21:22:08 2006 +0100
    63.3 @@ -204,7 +204,7 @@
    63.4    fun print _ _ = ();
    63.5  );
    63.6  
    63.7 -val _ = Context.add_setup [ContextData.init];
    63.8 +val _ = Context.add_setup ContextData.init;
    63.9  
   63.10  fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
   63.11  
    64.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Jan 19 15:45:10 2006 +0100
    64.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Jan 19 21:22:08 2006 +0100
    64.3 @@ -23,7 +23,7 @@
    64.4    if ! quick_and_dirty then prop
    64.5    else error "Proof may be skipped in quick_and_dirty mode only!";
    64.6  
    64.7 -val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
    64.8 +val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
    64.9  
   64.10  
   64.11  (* basic cheating *)
    65.1 --- a/src/Pure/Isar/term_style.ML	Thu Jan 19 15:45:10 2006 +0100
    65.2 +++ b/src/Pure/Isar/term_style.ML	Thu Jan 19 21:22:08 2006 +0100
    65.3 @@ -33,7 +33,7 @@
    65.4    fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
    65.5  end);
    65.6  
    65.7 -val _ = Context.add_setup [StyleData.init];
    65.8 +val _ = Context.add_setup StyleData.init;
    65.9  val print_styles = StyleData.print;
   65.10  
   65.11  
   65.12 @@ -68,26 +68,27 @@
   65.13    end;
   65.14  
   65.15  val _ = Context.add_setup
   65.16 - [add_style "lhs" (fst oo style_binargs),
   65.17 -  add_style "rhs" (snd oo style_binargs),
   65.18 -  add_style "prem1" (style_parm_premise 1),
   65.19 -  add_style "prem2" (style_parm_premise 2),
   65.20 -  add_style "prem3" (style_parm_premise 3),
   65.21 -  add_style "prem4" (style_parm_premise 4),
   65.22 -  add_style "prem5" (style_parm_premise 5),
   65.23 -  add_style "prem6" (style_parm_premise 6),
   65.24 -  add_style "prem7" (style_parm_premise 7),
   65.25 -  add_style "prem8" (style_parm_premise 8),
   65.26 -  add_style "prem9" (style_parm_premise 9),
   65.27 -  add_style "prem10" (style_parm_premise 10),
   65.28 -  add_style "prem11" (style_parm_premise 11),
   65.29 -  add_style "prem12" (style_parm_premise 12),
   65.30 -  add_style "prem13" (style_parm_premise 13),
   65.31 -  add_style "prem14" (style_parm_premise 14),
   65.32 -  add_style "prem15" (style_parm_premise 15),
   65.33 -  add_style "prem16" (style_parm_premise 16),
   65.34 -  add_style "prem17" (style_parm_premise 17),
   65.35 -  add_style "prem18" (style_parm_premise 18),
   65.36 -  add_style "prem19" (style_parm_premise 19),
   65.37 -  add_style "concl" (K Logic.strip_imp_concl)];
   65.38 + (add_style "lhs" (fst oo style_binargs) #>
   65.39 +  add_style "rhs" (snd oo style_binargs) #>
   65.40 +  add_style "prem1" (style_parm_premise 1) #>
   65.41 +  add_style "prem2" (style_parm_premise 2) #>
   65.42 +  add_style "prem3" (style_parm_premise 3) #>
   65.43 +  add_style "prem4" (style_parm_premise 4) #>
   65.44 +  add_style "prem5" (style_parm_premise 5) #>
   65.45 +  add_style "prem6" (style_parm_premise 6) #>
   65.46 +  add_style "prem7" (style_parm_premise 7) #>
   65.47 +  add_style "prem8" (style_parm_premise 8) #>
   65.48 +  add_style "prem9" (style_parm_premise 9) #>
   65.49 +  add_style "prem10" (style_parm_premise 10) #>
   65.50 +  add_style "prem11" (style_parm_premise 11) #>
   65.51 +  add_style "prem12" (style_parm_premise 12) #>
   65.52 +  add_style "prem13" (style_parm_premise 13) #>
   65.53 +  add_style "prem14" (style_parm_premise 14) #>
   65.54 +  add_style "prem15" (style_parm_premise 15) #>
   65.55 +  add_style "prem16" (style_parm_premise 16) #>
   65.56 +  add_style "prem17" (style_parm_premise 17) #>
   65.57 +  add_style "prem18" (style_parm_premise 18) #>
   65.58 +  add_style "prem19" (style_parm_premise 19) #>
   65.59 +  add_style "concl" (K Logic.strip_imp_concl));
   65.60 +
   65.61  end;
    66.1 --- a/src/Pure/Proof/extraction.ML	Thu Jan 19 15:45:10 2006 +0100
    66.2 +++ b/src/Pure/Proof/extraction.ML	Thu Jan 19 21:22:08 2006 +0100
    66.3 @@ -214,7 +214,7 @@
    66.4    fun print _ _ = ();
    66.5  end);
    66.6  
    66.7 -val _ = Context.add_setup [ExtractionData.init];
    66.8 +val _ = Context.add_setup ExtractionData.init;
    66.9  
   66.10  fun read_condeq thy =
   66.11    let val thy' = add_syntax thy
   66.12 @@ -401,7 +401,7 @@
   66.13  (** Pure setup **)
   66.14  
   66.15  val _ = Context.add_setup
   66.16 -  [add_types [("prop", ([], NONE))],
   66.17 +  (add_types [("prop", ([], NONE))] #>
   66.18  
   66.19     add_typeof_eqns
   66.20       ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
   66.21 @@ -422,7 +422,7 @@
   66.22      \    (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))",
   66.23  
   66.24        "(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==>  \
   66.25 -    \    (typeof (f)) == (Type (TYPE('f)))"],
   66.26 +    \    (typeof (f)) == (Type (TYPE('f)))"] #>
   66.27  
   66.28     add_realizes_eqns
   66.29       ["(typeof (PROP P)) == (Type (TYPE(Null))) ==>  \
   66.30 @@ -442,12 +442,12 @@
   66.31      \    (!!x. PROP realizes (Null) (PROP P (x)))",
   66.32  
   66.33        "(realizes (r) (!!x. PROP P (x))) ==  \
   66.34 -    \  (!!x. PROP realizes (r (x)) (PROP P (x)))"],
   66.35 +    \  (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
   66.36  
   66.37     Attrib.add_attributes
   66.38       [("extraction_expand",
   66.39         (Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
   66.40 -       "specify theorems / definitions to be expanded during extraction")]];
   66.41 +       "specify theorems / definitions to be expanded during extraction")]);
   66.42  
   66.43  
   66.44  (**** extract program ****)
    67.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jan 19 15:45:10 2006 +0100
    67.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jan 19 21:22:08 2006 +0100
    67.3 @@ -181,7 +181,7 @@
    67.4    in rew' end;
    67.5  
    67.6  fun rprocs b = [("Pure/meta_equality", rew b)];
    67.7 -val _ = Context.add_setup [Proofterm.add_prf_rprocs (rprocs false)];
    67.8 +val _ = Context.add_setup (Proofterm.add_prf_rprocs (rprocs false));
    67.9  
   67.10  
   67.11  (**** apply rewriting function to all terms in proof ****)
    68.1 --- a/src/Pure/Thy/html.ML	Thu Jan 19 15:45:10 2006 +0100
    68.2 +++ b/src/Pure/Thy/html.ML	Thu Jan 19 21:22:08 2006 +0100
    68.3 @@ -253,7 +253,7 @@
    68.4    ("var",   style "var"),
    68.5    ("xstr",  style "xstr")];
    68.6  
    68.7 -val _ = Context.add_setup [Theory.add_mode_tokentrfuns htmlN html_trans];
    68.8 +val _ = Context.add_setup (Theory.add_mode_tokentrfuns htmlN html_trans);
    68.9  
   68.10  
   68.11  
    69.1 --- a/src/Pure/Thy/present.ML	Thu Jan 19 15:45:10 2006 +0100
    69.2 +++ b/src/Pure/Thy/present.ML	Thu Jan 19 21:22:08 2006 +0100
    69.3 @@ -83,7 +83,7 @@
    69.4    fun print _ _ = ();
    69.5  end);
    69.6  
    69.7 -val _ = Context.add_setup [BrowserInfoData.init];
    69.8 +val _ = Context.add_setup BrowserInfoData.init;
    69.9  
   69.10  fun get_info thy =
   69.11    if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
    70.1 --- a/src/Pure/Tools/class_package.ML	Thu Jan 19 15:45:10 2006 +0100
    70.2 +++ b/src/Pure/Tools/class_package.ML	Thu Jan 19 21:22:08 2006 +0100
    70.3 @@ -39,7 +39,7 @@
    70.4  struct
    70.5  
    70.6  
    70.7 -(* data kind 'Pure/classes' *)
    70.8 +(* theory data *)
    70.9  
   70.10  type class_data = {
   70.11    superclasses: class list,
   70.12 @@ -87,6 +87,7 @@
   70.13    end
   70.14  );
   70.15  
   70.16 +val _ = Context.add_setup ClassData.init;
   70.17  val print_classes = ClassData.print;
   70.18  
   70.19  val lookup_class_data = Symtab.lookup o fst o ClassData.get;
   70.20 @@ -451,9 +452,4 @@
   70.21  
   70.22  end; (* local *)
   70.23  
   70.24 -
   70.25 -(* setup *)
   70.26 -
   70.27 -val _ = Context.add_setup [ClassData.init];
   70.28 -
   70.29  end; (* struct *)
    71.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Jan 19 15:45:10 2006 +0100
    71.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Jan 19 21:22:08 2006 +0100
    71.3 @@ -304,9 +304,11 @@
    71.4      target_data = Symtab.join (K (merge_target_data #> SOME))
    71.5        (target_data1, target_data2)
    71.6    };
    71.7 -  fun print thy _ = writeln "sorry, this stuff is too complicated...";
    71.8 +  fun print _ _ = ();
    71.9  end);
   71.10  
   71.11 +val _ = Context.add_setup CodegenData.init;
   71.12 +
   71.13  fun map_codegen_data f thy =
   71.14    case CodegenData.get thy
   71.15     of { modl, gens, target_data, logic_data } =>
   71.16 @@ -1311,18 +1313,17 @@
   71.17  
   71.18  
   71.19  
   71.20 -(** setup **)
   71.21 +(** theory setup **)
   71.22  
   71.23 -val _ = Context.add_setup [
   71.24 -  CodegenData.init,
   71.25 -(*   add_appconst_i ("op =", ((2, 2), appgen_eq)),  *)
   71.26 -  add_eqextr ("defs", eqextr_defs),
   71.27 -  add_defgen ("clsdecl", defgen_clsdecl),
   71.28 -  add_defgen ("funs", defgen_funs),
   71.29 -  add_defgen ("clsmem", defgen_clsmem),
   71.30 -  add_defgen ("datatypecons", defgen_datatypecons)(*,
   71.31 -  add_defgen ("clsinst", defgen_clsinst)  *)
   71.32 -];
   71.33 +val _ = Context.add_setup
   71.34 + (add_eqextr ("defs", eqextr_defs) #>
   71.35 +  add_defgen ("clsdecl", defgen_clsdecl) #>
   71.36 +  add_defgen ("funs", defgen_funs) #>
   71.37 +  add_defgen ("clsmem", defgen_clsmem) #>
   71.38 +  add_defgen ("datatypecons", defgen_datatypecons));
   71.39 +
   71.40 +(*   add_appconst_i ("op =", ((2, 2), appgen_eq))  *)
   71.41 +(*   add_defgen ("clsinst", defgen_clsinst)  *)
   71.42  
   71.43  end; (* local *)
   71.44  
    72.1 --- a/src/Pure/Tools/compute.ML	Thu Jan 19 15:45:10 2006 +0100
    72.2 +++ b/src/Pure/Tools/compute.ML	Thu Jan 19 21:22:08 2006 +0100
    72.3 @@ -277,7 +277,9 @@
    72.4  
    72.5  fun rewrite r ct = rewrite_param r default_naming ct
    72.6  
    72.7 -(* setup of the Pure.compute oracle *)
    72.8 +
    72.9 +(* theory setup *)
   72.10 +
   72.11  fun compute_oracle (thy, Param (r, naming, ct)) =
   72.12      let
   72.13          val _ = Theory.assert_super (theory_of r) thy
   72.14 @@ -286,6 +288,6 @@
   72.15          Logic.mk_equals (term_of ct, t')
   72.16      end
   72.17  
   72.18 -val _ = Context.add_setup [Theory.add_oracle ("compute", compute_oracle)]
   72.19 +val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle))
   72.20  
   72.21  end
    73.1 --- a/src/Pure/axclass.ML	Thu Jan 19 15:45:10 2006 +0100
    73.2 +++ b/src/Pure/axclass.ML	Thu Jan 19 21:22:08 2006 +0100
    73.3 @@ -136,7 +136,7 @@
    73.4      in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
    73.5  end);
    73.6  
    73.7 -val _ = Context.add_setup [AxclassesData.init];
    73.8 +val _ = Context.add_setup AxclassesData.init;
    73.9  val print_axclasses = AxclassesData.print;
   73.10  
   73.11  
   73.12 @@ -334,10 +334,10 @@
   73.13    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   73.14      default_intro_classes_tac facts;
   73.15  
   73.16 -val _ = Context.add_setup [Method.add_methods
   73.17 +val _ = Context.add_setup (Method.add_methods
   73.18   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   73.19 -   "back-chain introduction rules of axiomatic type classes"),
   73.20 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
   73.21 +    "back-chain introduction rules of axiomatic type classes"),
   73.22 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]);
   73.23  
   73.24  
   73.25  
    74.1 --- a/src/Pure/codegen.ML	Thu Jan 19 15:45:10 2006 +0100
    74.2 +++ b/src/Pure/codegen.ML	Thu Jan 19 21:22:08 2006 +0100
    74.3 @@ -240,7 +240,7 @@
    74.4         Pretty.strs ("type code generators:" :: map fst tycodegens)]);
    74.5  end);
    74.6  
    74.7 -val _ = Context.add_setup [CodegenData.init];
    74.8 +val _ = Context.add_setup CodegenData.init;
    74.9  val print_codegens = CodegenData.print;
   74.10  
   74.11  
   74.12 @@ -316,9 +316,9 @@
   74.13      (#attrs (CodegenData.get thy)))));
   74.14  
   74.15  val _ = Context.add_setup
   74.16 - [Attrib.add_attributes
   74.17 + (Attrib.add_attributes
   74.18    [("code", (code_attr, K Attrib.undef_local_attribute),
   74.19 -     "declare theorems for code generation")]];
   74.20 +     "declare theorems for code generation")]);
   74.21  
   74.22  
   74.23  (**** preprocessors ****)
   74.24 @@ -361,7 +361,7 @@
   74.25        end)
   74.26    in (add_preprocessor prep thy, eqn) end;
   74.27  
   74.28 -val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];
   74.29 +val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr));
   74.30  
   74.31  
   74.32  (**** associate constants with target language code ****)
   74.33 @@ -834,8 +834,8 @@
   74.34             end);
   74.35  
   74.36  val _ = Context.add_setup
   74.37 - [add_codegen "default" default_codegen,
   74.38 -  add_tycodegen "default" default_tycodegen];
   74.39 + (add_codegen "default" default_codegen #>
   74.40 +  add_tycodegen "default" default_tycodegen);
   74.41  
   74.42  
   74.43  fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
   74.44 @@ -1086,7 +1086,7 @@
   74.45     | _ => error ("Malformed annotation: " ^ quote s));
   74.46  
   74.47  val _ = Context.add_setup
   74.48 -  [assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
   74.49 +  (assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
   74.50       [("term_of",
   74.51         "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
   74.52        ("test",
   74.53 @@ -1098,7 +1098,7 @@
   74.54         \        val y = G i;\n\
   74.55         \        val f' = !f\n\
   74.56         \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
   74.57 -       \  in (fn x => !f x) end;\n")]))]];
   74.58 +       \  in (fn x => !f x) end;\n")]))]);
   74.59  
   74.60  
   74.61  structure P = OuterParse and K = OuterKeyword;
    75.1 --- a/src/Pure/proof_general.ML	Thu Jan 19 15:45:10 2006 +0100
    75.2 +++ b/src/Pure/proof_general.ML	Thu Jan 19 21:22:08 2006 +0100
    75.3 @@ -148,7 +148,7 @@
    75.4  
    75.5  in
    75.6  
    75.7 -val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];
    75.8 +val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
    75.9  
   75.10  end;
   75.11  
    76.1 --- a/src/Pure/simplifier.ML	Thu Jan 19 15:45:10 2006 +0100
    76.2 +++ b/src/Pure/simplifier.ML	Thu Jan 19 21:22:08 2006 +0100
    76.3 @@ -73,8 +73,8 @@
    76.4    val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
    76.5    val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    76.6    val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
    76.7 -    -> (theory -> theory) list
    76.8 -  val easy_setup: thm -> thm list -> (theory -> theory) list
    76.9 +    -> theory -> theory
   76.10 +  val easy_setup: thm -> thm list -> theory -> theory
   76.11  end;
   76.12  
   76.13  structure Simplifier: SIMPLIFIER =
   76.14 @@ -96,7 +96,7 @@
   76.15    fun print _ (ref ss) = print_ss ss;
   76.16  end);
   76.17  
   76.18 -val _ = Context.add_setup [GlobalSimpset.init];
   76.19 +val _ = Context.add_setup GlobalSimpset.init;
   76.20  val print_simpset = GlobalSimpset.print;
   76.21  val get_simpset = ! o GlobalSimpset.get;
   76.22  
   76.23 @@ -128,7 +128,7 @@
   76.24    fun print _ ss = print_ss ss;
   76.25  end);
   76.26  
   76.27 -val _ = Context.add_setup [LocalSimpset.init];
   76.28 +val _ = Context.add_setup LocalSimpset.init;
   76.29  val print_local_simpset = LocalSimpset.print;
   76.30  val get_local_simpset = LocalSimpset.get;
   76.31  val put_local_simpset = LocalSimpset.put;
   76.32 @@ -260,12 +260,12 @@
   76.33  (* setup attributes *)
   76.34  
   76.35  val _ = Context.add_setup
   76.36 - [Attrib.add_attributes
   76.37 + (Attrib.add_attributes
   76.38     [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
   76.39        "declaration of Simplifier rule"),
   76.40      (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
   76.41        "declaration of Simplifier congruence rule"),
   76.42 -    ("simplified", Attrib.common simplified, "simplified rule")]];
   76.43 +    ("simplified", Attrib.common simplified, "simplified rule")]);
   76.44  
   76.45  
   76.46  
   76.47 @@ -318,18 +318,14 @@
   76.48        ((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
   76.49  
   76.50  
   76.51 -(* setup methods *)
   76.52  
   76.53 -fun setup_methods more_mods = Method.add_methods
   76.54 +(** setup **)
   76.55 +
   76.56 +fun method_setup more_mods = Method.add_methods
   76.57   [(simpN, simp_args more_mods simp_method', "simplification"),
   76.58    ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
   76.59  
   76.60 -fun method_setup mods = [setup_methods mods];
   76.61 -
   76.62 -
   76.63 -(** easy_setup **)
   76.64 -
   76.65 -fun easy_setup reflect trivs =
   76.66 +fun easy_setup reflect trivs = method_setup [] #> (fn thy =>
   76.67    let
   76.68      val trivialities = Drule.reflexive_thm :: trivs;
   76.69  
   76.70 @@ -345,14 +341,14 @@
   76.71        else [thm RS reflect] handle THM _ => [];
   76.72  
   76.73      fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   76.74 -
   76.75 -    fun init_ss thy =
   76.76 -      (GlobalSimpset.get thy :=
   76.77 -        empty_ss setsubgoaler asm_simp_tac
   76.78 -        setSSolver safe_solver
   76.79 -        setSolver unsafe_solver
   76.80 -        setmksimps mksimps; thy);
   76.81 -  in method_setup [] @ [init_ss] end;
   76.82 +  in
   76.83 +    GlobalSimpset.get thy :=
   76.84 +      empty_ss setsubgoaler asm_simp_tac
   76.85 +      setSSolver safe_solver
   76.86 +      setSolver unsafe_solver
   76.87 +      setmksimps mksimps;
   76.88 +    thy
   76.89 +  end);
   76.90  
   76.91  
   76.92  open MetaSimplifier;
    77.1 --- a/src/Sequents/prover.ML	Thu Jan 19 15:45:10 2006 +0100
    77.2 +++ b/src/Sequents/prover.ML	Thu Jan 19 21:22:08 2006 +0100
    77.3 @@ -179,7 +179,7 @@
    77.4    fun print _ (ref pack) = print_pack pack;
    77.5  end);
    77.6  
    77.7 -val prover_setup = [ProverData.init];
    77.8 +val prover_setup = ProverData.init;
    77.9  
   77.10  val print_pack = ProverData.print;
   77.11  val pack_ref_of = ProverData.get;
    78.1 --- a/src/ZF/Tools/ind_cases.ML	Thu Jan 19 15:45:10 2006 +0100
    78.2 +++ b/src/ZF/Tools/ind_cases.ML	Thu Jan 19 21:22:08 2006 +0100
    78.3 @@ -9,7 +9,7 @@
    78.4  sig
    78.5    val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
    78.6    val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    78.7 -  val setup: (theory -> theory) list
    78.8 +  val setup: theory -> theory
    78.9  end;
   78.10  
   78.11  structure IndCases: IND_CASES =
   78.12 @@ -72,9 +72,9 @@
   78.13  (* package setup *)
   78.14  
   78.15  val setup =
   78.16 - [IndCasesData.init,
   78.17 + (IndCasesData.init #>
   78.18    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   78.19 -    "dynamic case analysis on sets")]];
   78.20 +    "dynamic case analysis on sets")]);
   78.21  
   78.22  
   78.23  (* outer syntax *)
    79.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Jan 19 15:45:10 2006 +0100
    79.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Jan 19 21:22:08 2006 +0100
    79.3 @@ -15,7 +15,7 @@
    79.4    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
    79.5    val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
    79.6      (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
    79.7 -  val setup: (theory -> theory) list
    79.8 +  val setup: theory -> theory
    79.9  end;
   79.10  
   79.11  
   79.12 @@ -185,13 +185,13 @@
   79.13  (* theory setup *)
   79.14  
   79.15  val setup =
   79.16 - [DatatypesData.init,
   79.17 -  ConstructorsData.init,
   79.18 + (DatatypesData.init #>
   79.19 +  ConstructorsData.init #>
   79.20    Method.add_methods
   79.21      [("induct_tac", Method.goal_args Args.name induct_tac,
   79.22        "induct_tac emulation (dynamic instantiation!)"),
   79.23       ("case_tac", Method.goal_args Args.name exhaust_tac,
   79.24 -      "datatype case_tac emulation (dynamic instantiation!)")]];
   79.25 +      "datatype case_tac emulation (dynamic instantiation!)")]);
   79.26  
   79.27  
   79.28  (* outer syntax *)
    80.1 --- a/src/ZF/Tools/numeral_syntax.ML	Thu Jan 19 15:45:10 2006 +0100
    80.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Thu Jan 19 21:22:08 2006 +0100
    80.3 @@ -12,7 +12,7 @@
    80.4    val mk_bin   : IntInf.int -> term
    80.5    val int_tr   : term list -> term
    80.6    val int_tr'  : bool -> typ -> term list -> term
    80.7 -  val setup    : (theory -> theory) list
    80.8 +  val setup    : theory -> theory
    80.9  end;
   80.10  
   80.11  structure NumeralSyntax: NUMERAL_SYNTAX =
   80.12 @@ -100,7 +100,7 @@
   80.13  
   80.14  
   80.15  val setup =
   80.16 - [Theory.add_trfuns ([], [("_Int", int_tr)], [], []),
   80.17 -  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]];
   80.18 + (Theory.add_trfuns ([], [("_Int", int_tr)], [], []) #>
   80.19 +  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
   80.20  
   80.21  end;
    81.1 --- a/src/ZF/Tools/typechk.ML	Thu Jan 19 15:45:10 2006 +0100
    81.2 +++ b/src/ZF/Tools/typechk.ML	Thu Jan 19 21:22:08 2006 +0100
    81.3 @@ -37,7 +37,7 @@
    81.4  signature TYPE_CHECK =
    81.5  sig
    81.6    include BASIC_TYPE_CHECK
    81.7 -  val setup: (theory -> theory) list
    81.8 +  val setup: theory -> theory
    81.9  end;
   81.10  
   81.11  structure TypeCheck: TYPE_CHECK =
   81.12 @@ -210,10 +210,11 @@
   81.13  (** theory setup **)
   81.14  
   81.15  val setup =
   81.16 - [TypecheckingData.init, LocalTypecheckingData.init,
   81.17 -  fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy),
   81.18 -  Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
   81.19 -  Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
   81.20 + (TypecheckingData.init #>
   81.21 +  LocalTypecheckingData.init #>
   81.22 +  (fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy)) #>
   81.23 +  Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")] #>
   81.24 +  Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]);
   81.25  
   81.26  
   81.27  (** outer syntax **)