added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
proper name bindings;

--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Mon May 02 13:29:47 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon May 02 16:33:21 2011 +0200
@@ -593,14 +593,14 @@
   \begin{mldecls}
   @{index_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\
   @{index_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\
-  @{index_ML Attrib.config_bool: "string -> (Context.generic -> bool) ->
-  bool Config.T * (theory -> theory)"} \\
-  @{index_ML Attrib.config_int: "string -> (Context.generic -> int) ->
-  int Config.T * (theory -> theory)"} \\
-  @{index_ML Attrib.config_real: "string -> (Context.generic -> real) ->
-  real Config.T * (theory -> theory)"} \\
-  @{index_ML Attrib.config_string: "string -> (Context.generic -> string) ->
-  string Config.T * (theory -> theory)"} \\
+  @{index_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) ->
+  bool Config.T"} \\
+  @{index_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) ->
+  int Config.T"} \\
+  @{index_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) ->
+  real Config.T"} \\
+  @{index_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) ->
+  string Config.T"} \\
   \end{mldecls}
 
   \begin{description}
@@ -611,13 +611,13 @@
   \item @{ML Config.map}~@{text "config f ctxt"} updates the context
   by updating the value of @{text "config"}.
 
-  \item @{text "(config, setup) ="}~@{ML Attrib.config_bool}~@{text
-  "name default"} creates a named configuration option of type
-  @{ML_type bool}, with the given @{text "default"} depending on the
-  application context.  The resulting @{text "config"} can be used to
-  get/map its value in a given context.  The @{text "setup"} function
-  needs to be applied to the theory initially, in order to make
-  concrete declaration syntax available to the user.
+  \item @{text "config ="}~@{ML Attrib.setup_config_bool}~@{text "name
+  default"} creates a named configuration option of type @{ML_type
+  bool}, with the given @{text "default"} depending on the application
+  context.  The resulting @{text "config"} can be used to get/map its
+  value in a given context.  There is an implicit update of the
+  background theory that registers the option as attribute with some
+  concrete syntax.
 
   \item @{ML Attrib.config_int}, @{ML Attrib.config_real}, and @{ML
   Attrib.config_string} work like @{ML Attrib.config_bool}, but for
@@ -631,10 +631,9 @@
   default value @{ML false}.  *}
 
 ML {*
-  val (my_flag, my_flag_setup) =
-    Attrib.config_bool "my_flag" (K false)
+  val my_flag =
+    Attrib.setup_config_bool @{binding my_flag} (K false)
 *}
-setup my_flag_setup
 
 text {* Now the user can refer to @{attribute my_flag} in
   declarations, while ML tools can retrieve the current value from the
@@ -659,10 +658,9 @@
   (floating-point numbers). *}
 
 ML {*
-  val (airspeed_velocity, airspeed_velocity_setup) =
-    Attrib.config_real "airspeed_velocity" (K 0.0)
+  val airspeed_velocity =
+    Attrib.setup_config_real @{binding airspeed_velocity} (K 0.0)
 *}
-setup airspeed_velocity_setup
 
 declare [[airspeed_velocity = 10]]
 declare [[airspeed_velocity = 9.9]]

--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon May 02 13:29:47 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon May 02 16:33:21 2011 +0200
@@ -797,14 +797,14 @@
 \begin{mldecls}
   \indexdef{}{ML}{Config.get}\verb|Config.get: Proof.context -> 'a Config.T -> 'a| \\
   \indexdef{}{ML}{Config.map}\verb|Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context| \\
-  \indexdef{}{ML}{Attrib.config\_bool}\verb|Attrib.config_bool: string -> (Context.generic -> bool) ->|\isasep\isanewline%
-\verb|  bool Config.T * (theory -> theory)| \\
-  \indexdef{}{ML}{Attrib.config\_int}\verb|Attrib.config_int: string -> (Context.generic -> int) ->|\isasep\isanewline%
-\verb|  int Config.T * (theory -> theory)| \\
-  \indexdef{}{ML}{Attrib.config\_real}\verb|Attrib.config_real: string -> (Context.generic -> real) ->|\isasep\isanewline%
-\verb|  real Config.T * (theory -> theory)| \\
-  \indexdef{}{ML}{Attrib.config\_string}\verb|Attrib.config_string: string -> (Context.generic -> string) ->|\isasep\isanewline%
-\verb|  string Config.T * (theory -> theory)| \\
+  \indexdef{}{ML}{Attrib.setup\_config\_bool}\verb|Attrib.setup_config_bool: binding -> (Context.generic -> bool) ->|\isasep\isanewline%
+\verb|  bool Config.T| \\
+  \indexdef{}{ML}{Attrib.setup\_config\_int}\verb|Attrib.setup_config_int: binding -> (Context.generic -> int) ->|\isasep\isanewline%
+\verb|  int Config.T| \\
+  \indexdef{}{ML}{Attrib.setup\_config\_real}\verb|Attrib.setup_config_real: binding -> (Context.generic -> real) ->|\isasep\isanewline%
+\verb|  real Config.T| \\
+  \indexdef{}{ML}{Attrib.setup\_config\_string}\verb|Attrib.setup_config_string: binding -> (Context.generic -> string) ->|\isasep\isanewline%
+\verb|  string Config.T| \\
   \end{mldecls}
 
   \begin{description}
@@ -815,12 +815,11 @@
   \item \verb|Config.map|~\isa{config\ f\ ctxt} updates the context
   by updating the value of \isa{config}.
 
-  \item \isa{{\isaliteral{28}{\isacharparenleft}}config{\isaliteral{2C}{\isacharcomma}}\ setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}}~\verb|Attrib.config_bool|~\isa{name\ default} creates a named configuration option of type
-  \verb|bool|, with the given \isa{default} depending on the
-  application context.  The resulting \isa{config} can be used to
-  get/map its value in a given context.  The \isa{setup} function
-  needs to be applied to the theory initially, in order to make
-  concrete declaration syntax available to the user.
+  \item \isa{config\ {\isaliteral{3D}{\isacharequal}}}~\verb|Attrib.setup_config_bool|~\isa{name\ default} creates a named configuration option of type \verb|bool|, with the given \isa{default} depending on the application
+  context.  The resulting \isa{config} can be used to get/map its
+  value in a given context.  There is an implicit update of the
+  background theory that registers the option as attribute with some
+  concrete syntax.
 
   \item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for
   types \verb|int| and \verb|string|, respectively.
@@ -863,11 +862,13 @@
 \isatagML
 \isacommand{ML}\isamarkupfalse%
 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ val\ {\isaliteral{28}{\isacharparenleft}}my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{2C}{\isacharcomma}}\ my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}config{\isaliteral{5F}{\isacharunderscore}}bool\ {\isaliteral{22}{\isachardoublequote}}my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{setup}\isamarkupfalse%
-\ my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{5F}{\isacharunderscore}}setup%
+\ \ val\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}bool\ %
+\isaantiq
+binding\ my{\isaliteral{5F}{\isacharunderscore}}flag{}%
+\endisaantiq
+\ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{2A7D}{\isacharverbatimclose}}%
 \endisatagML
 {\isafoldML}%
 %
@@ -1028,11 +1029,13 @@
 \isatagML
 \isacommand{ML}\isamarkupfalse%
 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ val\ {\isaliteral{28}{\isacharparenleft}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{2C}{\isacharcomma}}\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}config{\isaliteral{5F}{\isacharunderscore}}real\ {\isaliteral{22}{\isachardoublequote}}airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{setup}\isamarkupfalse%
-\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{5F}{\isacharunderscore}}setup%
+\ \ val\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}real\ %
+\isaantiq
+binding\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{}%
+\endisaantiq
+\ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{2A7D}{\isacharverbatimclose}}%
 \endisatagML
 {\isafoldML}%
 %

--- a/src/FOLP/IFOLP.thy	Mon May 02 13:29:47 2011 +0200
+++ b/src/FOLP/IFOLP.thy	Mon May 02 16:33:21 2011 +0200
@@ -69,8 +69,7 @@
 *}
 
 (*show_proofs = true displays the proof terms -- they are ENORMOUS*)
-ML {* val (show_proofs, setup_show_proofs) = Attrib.config_bool "show_proofs" (K false) *}
-setup setup_show_proofs
+ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *}
 
 print_translation (advanced) {*
   let

--- a/src/HOL/Library/Sum_of_Squares.thy	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares.thy	Mon May 02 16:33:21 2011 +0200
@@ -38,7 +38,6 @@
   the proof without calling an external prover.
 *}
 
-setup Sum_of_Squares.setup
 setup SOS_Wrapper.setup
 
 text {* Tests *}

--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon May 02 16:33:21 2011 +0200
@@ -24,7 +24,7 @@
 
 (*** calling provers ***)
 
-val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "")
+val dest_dir = Attrib.setup_config_string @{binding sos_dest_dir} (K "")
 
 fun filename dir name =
   let
@@ -117,7 +117,7 @@
   | prover "csdp" = csdp
   | prover name = error ("Unknown prover: " ^ name)
 
-val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp")
+val prover_name = Attrib.setup_config_string @{binding sos_prover_name} (K "remote_csdp")
 
 fun call_solver ctxt opt_name =
   let
@@ -140,8 +140,6 @@
 fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method
 
 val setup =
-  setup_dest_dir #>
-  setup_prover_name #>
   Method.setup @{binding sos}
     (Scan.lift (Scan.option Parse.xname)
       >> (fn opt_name => fn ctxt =>

--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon May 02 16:33:21 2011 +0200
@@ -10,7 +10,6 @@
   datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
   val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
   val trace: bool Config.T
-  val setup: theory -> theory
   exception Failure of string;
 end
 
@@ -50,8 +49,7 @@
 val pow2 = rat_pow rat_2;
 val pow10 = rat_pow rat_10;
 
-val (trace, setup_trace) = Attrib.config_bool "sos_trace" (K false);
-val setup = setup_trace;
+val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
 
 exception Sanity;
 

--- a/src/HOL/Meson.thy	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Meson.thy	Mon May 02 16:33:21 2011 +0200
@@ -192,10 +192,7 @@
 use "Tools/Meson/meson_clausify.ML"
 use "Tools/Meson/meson_tactic.ML"
 
-setup {*
-  Meson.setup
-  #> Meson_Tactic.setup
-*}
+setup {* Meson_Tactic.setup *}
 
 hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
 hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD

--- a/src/HOL/Metis.thy	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Metis.thy	Mon May 02 16:33:21 2011 +0200
@@ -63,10 +63,7 @@
 use "Tools/Metis/metis_reconstruct.ML"
 use "Tools/Metis/metis_tactics.ML"
 
-setup {*
-  Metis_Reconstruct.setup
-  #> Metis_Tactics.setup
-*}
+setup {* Metis_Tactics.setup *}
 
 hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
 hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def

--- a/src/HOL/Mirabelle/Mirabelle.thy	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy	Mon May 02 16:33:21 2011 +0200
@@ -14,8 +14,6 @@
 
 ML {* Toplevel.add_hook Mirabelle.step_hook *}
 
-setup Mirabelle.setup
-
 ML {*
 signature MIRABELLE_ACTION =
 sig

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 02 16:33:21 2011 +0200
@@ -9,7 +9,6 @@
   val timeout : int Config.T
   val start_line : int Config.T
   val end_line : int Config.T
-  val setup : theory -> theory
 
   (*core*)
   type init_action = int -> theory -> theory
@@ -43,12 +42,10 @@
 
 (* Mirabelle configuration *)
 
-val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" (K "")
-val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" (K 30)
-val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" (K 0)
-val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" (K ~1)
-
-val setup = setup1 #> setup2 #> setup3 #> setup4
+val logfile = Attrib.setup_config_string @{binding mirabelle_logfile} (K "")
+val timeout = Attrib.setup_config_int @{binding mirabelle_timeout} (K 30)
+val start_line = Attrib.setup_config_int @{binding mirabelle_start_line} (K 0)
+val end_line = Attrib.setup_config_int @{binding mirabelle_end_line} (K ~1)
 
 
 (* Mirabelle core *)

--- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon May 02 16:33:21 2011 +0200
@@ -42,8 +42,7 @@
 (* equality-lemma can be derived. *)
 exception EQVT_FORM of string
 
-val (nominal_eqvt_debug, setup_nominal_eqvt_debug) =
-  Attrib.config_bool "nominal_eqvt_debug" (K false);
+val nominal_eqvt_debug = Attrib.setup_config_bool @{binding nominal_eqvt_debug} (K false);
 
 fun tactic ctxt (msg, tac) =
   if Config.get ctxt nominal_eqvt_debug
@@ -170,7 +169,6 @@
 val get_eqvt_thms = Context.Proof #> Data.get;
 
 val setup =
-  setup_nominal_eqvt_debug #>
   Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
    "equivariance theorem declaration" #>
   Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)

--- a/src/HOL/Sledgehammer.thy	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon May 02 16:33:21 2011 +0200
@@ -19,9 +19,6 @@
      "Tools/Sledgehammer/sledgehammer_isar.ML"
 begin
 
-setup {*
-  Sledgehammer_Provers.setup
-  #> Sledgehammer_Isar.setup
-*}
+setup {* Sledgehammer_Isar.setup *}
 
 end

--- a/src/HOL/Tools/Meson/meson.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Mon May 02 16:33:21 2011 +0200
@@ -40,19 +40,17 @@
   val make_meta_clause: thm -> thm
   val make_meta_clauses: thm list -> thm list
   val meson_tac: Proof.context -> thm list -> int -> tactic
-  val setup : theory -> theory
 end
 
 structure Meson : MESON =
 struct
 
-val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
+val trace = Attrib.setup_config_bool @{binding meson_trace} (K false)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
 val max_clauses_default = 60
-val (max_clauses, max_clauses_setup) =
-  Attrib.config_int "meson_max_clauses" (K max_clauses_default)
+val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K max_clauses_default)
 
 (*No known example (on 1-5-2007) needs even thirty*)
 val iter_deepen_limit = 50;
@@ -738,8 +736,4 @@
     name_thms "MClause#"
       (distinct Thm.eq_thm_prop (map make_meta_clause ths));
 
-val setup =
-  trace_setup
-  #> max_clauses_setup
-
 end;

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 02 16:33:21 2011 +0200
@@ -23,7 +23,6 @@
     -> (Metis_Thm.thm * thm) list
   val discharge_skolem_premises :
     Proof.context -> (thm * term) option list -> thm -> thm
-  val setup : theory -> theory
 end;
 
 structure Metis_Reconstruct : METIS_RECONSTRUCT =
@@ -31,8 +30,8 @@
 
 open Metis_Translate
 
-val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
-val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
+val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
+val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 fun verbose_warning ctxt msg =
@@ -897,6 +896,4 @@
                     \Error when discharging Skolem assumptions.")
     end
 
-val setup = trace_setup #> verbose_setup
-
 end;

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 02 16:33:21 2011 +0200
@@ -25,9 +25,8 @@
 open Metis_Translate
 open Metis_Reconstruct
 
-val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
-val (new_skolemizer, new_skolemizer_setup) =
-  Attrib.config_bool "metis_new_skolemizer" (K false)
+val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
+val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
 
 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
 
@@ -190,9 +189,7 @@
                end)))
 
 val setup =
-  type_lits_setup
-  #> new_skolemizer_setup
-  #> method @{binding metis} HO "Metis for FOL/HOL problems"
+  method @{binding metis} HO "Metis for FOL/HOL problems"
   #> method @{binding metisF} FO "Metis for FOL problems"
   #> method @{binding metisFT} FT
             "Metis for FOL/HOL problems with fully-typed translation"

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon May 02 16:33:21 2011 +0200
@@ -1570,12 +1570,11 @@
 
 (* values_timeout configuration *)
 
-val (values_timeout, setup_values_timeout) = Attrib.config_real "values_timeout" (K 20.0)
+val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K 20.0)
 
 val setup = PredData.put (Graph.empty) #>
   Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
     "adding alternative introduction rules for code generation of inductive predicates"
-  #> setup_values_timeout
 
 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
 (* FIXME ... this is important to avoid changing the background theory below *)

--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon May 02 16:33:21 2011 +0200
@@ -28,20 +28,11 @@
 
 (** dynamic options **)
 
-val (smart_quantifier, setup_smart_quantifier) =
-  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
-
-val (fast, setup_fast) =
-  Attrib.config_bool "quickcheck_fast" (K false)
-
-val (bounded_forall, setup_bounded_forall) =
-  Attrib.config_bool "quickcheck_bounded_forall" (K false)
-  
-val (full_support, setup_full_support) =
-  Attrib.config_bool "quickcheck_full_support" (K true)
-
-val (quickcheck_pretty, setup_quickcheck_pretty) =
-  Attrib.config_bool "quickcheck_pretty" (K true)
+val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
+val fast = Attrib.setup_config_bool @{binding quickcheck_fast} (K false)
+val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false)
+val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
+val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
  
 (** general term functions **)
 
@@ -508,11 +499,6 @@
       (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
-  #> setup_smart_quantifier
-  #> setup_full_support
-  #> setup_fast
-  #> setup_bounded_forall
-  #> setup_quickcheck_pretty
   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 02 16:33:21 2011 +0200
@@ -18,8 +18,7 @@
 
 (* configurations *)
 
-val (finite_functions, setup_finite_functions) =
-  Attrib.config_bool "quickcheck_finite_functions" (K true)
+val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
 
 (* narrowing specific names and types *)
 
@@ -208,7 +207,6 @@
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
-  #> setup_finite_functions
   #> Context.theory_map
     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
     

--- a/src/HOL/Tools/SMT/smt_config.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon May 02 16:33:21 2011 +0200
@@ -23,12 +23,10 @@
   (*options*)
   val oracle: bool Config.T
   val datatypes: bool Config.T
-  val timeoutN: string
   val timeout: real Config.T
   val random_seed: int Config.T
   val fixed: bool Config.T
   val verbose: bool Config.T
-  val traceN: string
   val trace: bool Config.T
   val trace_used_facts: bool Config.T
   val monomorph_limit: int Config.T
@@ -149,75 +147,21 @@
 
 (* options *)
 
-val oracleN = "smt_oracle"
-val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
-
-val datatypesN = "smt_datatypes"
-val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
-
-val timeoutN = "smt_timeout"
-val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
-
-val random_seedN = "smt_random_seed"
-val (random_seed, setup_random_seed) = Attrib.config_int random_seedN (K 1)
-
-val fixedN = "smt_fixed"
-val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
-
-val verboseN = "smt_verbose"
-val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
-
-val traceN = "smt_trace"
-val (trace, setup_trace) = Attrib.config_bool traceN (K false)
-
-val trace_used_factsN = "smt_trace_used_facts"
-val (trace_used_facts, setup_trace_used_facts) =
-  Attrib.config_bool trace_used_factsN (K false)
-
-val monomorph_limitN = "smt_monomorph_limit"
-val (monomorph_limit, setup_monomorph_limit) =
-  Attrib.config_int monomorph_limitN (K 10)
-
-val monomorph_instancesN = "smt_monomorph_instances"
-val (monomorph_instances, setup_monomorph_instances) =
-  Attrib.config_int monomorph_instancesN (K 500)
-
-val monomorph_fullN = "smt_monomorph_full"
-val (monomorph_full, setup_monomorph_full) =
-  Attrib.config_bool monomorph_fullN (K true)
-
-val infer_triggersN = "smt_infer_triggers"
-val (infer_triggers, setup_infer_triggers) =
-  Attrib.config_bool infer_triggersN (K false)
-
-val drop_bad_factsN = "smt_drop_bad_facts"
-val (drop_bad_facts, setup_drop_bad_facts) =
-  Attrib.config_bool drop_bad_factsN (K false)
-
-val filter_only_factsN = "smt_filter_only_facts"
-val (filter_only_facts, setup_filter_only_facts) =
-  Attrib.config_bool filter_only_factsN (K false)
-
-val debug_filesN = "smt_debug_files"
-val (debug_files, setup_debug_files) =
-  Attrib.config_string debug_filesN (K "")
-
-val setup_options =
-  setup_oracle #>
-  setup_datatypes #>
-  setup_timeout #>
-  setup_random_seed #>
-  setup_fixed #>
-  setup_trace #>
-  setup_verbose #>
-  setup_monomorph_limit #>
-  setup_monomorph_instances #>
-  setup_monomorph_full #>
-  setup_infer_triggers #>
-  setup_drop_bad_facts #>
-  setup_filter_only_facts #>
-  setup_trace_used_facts #>
-  setup_debug_files
+val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
+val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false)
+val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
+val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
+val fixed = Attrib.setup_config_bool @{binding smt_fixed} (K false)
+val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
+val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
+val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
+val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
+val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val monomorph_full = Attrib.setup_config_bool @{binding smt_monomorph_full} (K true)
+val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
+val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
+val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
+val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
 
 
 (* diagnostics *)
@@ -269,7 +213,6 @@
 
 val setup =
   setup_solver #>
-  setup_options #>
   setup_certificates
 
 fun print_setup ctxt =

--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Mon May 02 16:33:21 2011 +0200
@@ -43,7 +43,7 @@
   else if String.isPrefix unknown line then SMT_Solver.Unknown
   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
     quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
-    "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
+    "configuration option " ^ quote (Config.name_of SMT_Config.trace) ^ " and " ^
     "see the trace for details."))
 
 fun on_first_line test_outcome solver_name lines =

--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon May 02 16:33:21 2011 +0200
@@ -350,7 +350,7 @@
     | SMT_Failure.SMT (fail as SMT_Failure.Time_Out) =>
         error ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^
           SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^
-          "configuration option " ^ SMT_Config.timeoutN ^ " might help)")
+          "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")
     | SMT_Failure.SMT fail => error (str_of ctxt fail)
 
   fun tag_rules thms = map_index (apsnd (pair NONE)) thms

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 16:33:21 2011 +0200
@@ -96,7 +96,6 @@
   val running_provers : unit -> unit
   val messages : int option -> unit
   val get_prover : Proof.context -> bool -> string -> prover
-  val setup : theory -> theory
 end;
 
 structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
@@ -272,15 +271,15 @@
 
 (* configuration attributes *)
 
-val (dest_dir, dest_dir_setup) =
-  Attrib.config_string "sledgehammer_dest_dir" (K "")
+val dest_dir =
+  Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
   (* Empty string means create files in Isabelle's temporary files directory. *)
 
-val (problem_prefix, problem_prefix_setup) =
-  Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
+val problem_prefix =
+  Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
 
-val (measure_run_time, measure_run_time_setup) =
-  Attrib.config_bool "sledgehammer_measure_run_time" (K false)
+val measure_run_time =
+  Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
 
 fun with_path cleanup after f path =
   Exn.capture f path
@@ -806,9 +805,4 @@
       error ("No such prover: " ^ name ^ ".")
   end
 
-val setup =
-  dest_dir_setup
-  #> problem_prefix_setup
-  #> measure_run_time_setup
-
 end;

--- a/src/HOL/Tools/inductive_codegen.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 02 16:33:21 2011 +0200
@@ -862,10 +862,10 @@
       NONE => deepen bound f (i + 1)
     | SOME x => SOME x);
 
-val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" (K 10);
-val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" (K 1);
-val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
-val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
+val depth_bound = Attrib.setup_config_int @{binding ind_quickcheck_depth} (K 10);
+val depth_start = Attrib.setup_config_int @{binding ind_quickcheck_depth_start} (K 1);
+val random_values = Attrib.setup_config_int @{binding ind_quickcheck_random} (K 5);
+val size_offset = Attrib.setup_config_int @{binding ind_quickcheck_size_offset} (K 0);
 
 fun test_term ctxt [(t, [])] =
       let
@@ -925,10 +925,6 @@
       error "Compilation of multiple instances is not supported by tester SML_inductive";
 
 val quickcheck_setup =
-  setup_depth_bound #>
-  setup_depth_start #>
-  setup_random_values #>
-  setup_size_offset #>
   Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
 
 end;

--- a/src/HOL/Tools/lin_arith.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Mon May 02 16:33:21 2011 +0200
@@ -99,8 +99,8 @@
   {splits = splits, inj_consts = update (op =) c inj_consts,
    discrete = discrete});
 
-val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" (K 9);
-val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" (K 9);
+val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
+val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
 
 
 structure LA_Data =
@@ -905,7 +905,6 @@
       (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
 
 val global_setup =
-  setup_split_limit #> setup_neq_limit #>
   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
     "declaration of split rules for arithmetic procedure" #>
   Method.setup @{binding linarith}

--- a/src/Provers/blast.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/Provers/blast.ML	Mon May 02 16:33:21 2011 +0200
@@ -1269,7 +1269,8 @@
 (*Public version with fixed depth*)
 fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;
 
-val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
+val (depth_limit, setup_depth_limit) =
+  Attrib.config_int_global @{binding blast_depth_limit} (K 20);
 
 fun blast_tac cs i st =
     ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)

--- a/src/Pure/Isar/attrib.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon May 02 16:33:21 2011 +0200
@@ -36,15 +36,26 @@
   val multi_thm: thm list context_parser
   val print_configs: Proof.context -> unit
   val internal: (morphism -> attribute) -> src
-  val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
-  val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
-  val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
-  val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
-  val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
-  val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
-  val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
-  val config_string_global:
-    bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
+  val config_bool: Binding.binding ->
+    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
+  val config_int: Binding.binding ->
+    (Context.generic -> int) -> int Config.T * (theory -> theory)
+  val config_real: Binding.binding ->
+    (Context.generic -> real) -> real Config.T * (theory -> theory)
+  val config_string: Binding.binding ->
+    (Context.generic -> string) -> string Config.T * (theory -> theory)
+  val config_bool_global: Binding.binding ->
+    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
+  val config_int_global: Binding.binding ->
+    (Context.generic -> int) -> int Config.T * (theory -> theory)
+  val config_real_global: Binding.binding ->
+    (Context.generic -> real) -> real Config.T * (theory -> theory)
+  val config_string_global: Binding.binding ->
+    (Context.generic -> string) -> string Config.T * (theory -> theory)
+  val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
+  val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
+  val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
+  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
 end;
 
 structure Attrib: ATTRIB =
@@ -366,34 +377,53 @@
   let val config_type = Config.get_global thy config
   in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
 
-in
-
-fun register_config config thy =
-  let
-    val bname = Config.name_of config;
-    val name = Sign.full_bname thy bname;
-  in
+fun register binding config thy =
+  let val name = Sign.full_name thy binding in
     thy
-    |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
-      "configuration option"
+    |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option"
     |> Configs.map (Symtab.update (name, config))
   end;
 
-fun declare_config make coerce global name default =
+fun declare make coerce global binding default =
   let
+    val name = Binding.name_of binding;
     val config_value = Config.declare_generic {global = global} name (make o default);
     val config = coerce config_value;
-  in (config, register_config config_value) end;
+  in (config, register binding config_value) end;
+
+in
+
+val config_bool = declare Config.Bool Config.bool false;
+val config_int = declare Config.Int Config.int false;
+val config_real = declare Config.Real Config.real false;
+val config_string = declare Config.String Config.string false;
+
+val config_bool_global = declare Config.Bool Config.bool true;
+val config_int_global = declare Config.Int Config.int true;
+val config_real_global = declare Config.Real Config.real true;
+val config_string_global = declare Config.String Config.string true;
+
+fun register_config config = register (Binding.name (Config.name_of config)) config;
+
+end;
 
-val config_bool = declare_config Config.Bool Config.bool false;
-val config_int = declare_config Config.Int Config.int false;
-val config_real = declare_config Config.Real Config.real false;
-val config_string = declare_config Config.String Config.string false;
+
+(* implicit setup *)
+
+local
 
-val config_bool_global = declare_config Config.Bool Config.bool true;
-val config_int_global = declare_config Config.Int Config.int true;
-val config_real_global = declare_config Config.Real Config.real true;
-val config_string_global = declare_config Config.String Config.string true;
+fun setup_config declare_config binding default =
+  let
+    val (config, setup) = declare_config binding default;
+    val _ = Context.>> (Context.map_theory setup);
+  in config end;
+
+in
+
+val setup_config_bool = setup_config config_bool;
+val setup_config_int = setup_config config_int;
+val setup_config_string = setup_config config_string;
+val setup_config_real = setup_config config_real;
 
 end;
 

--- a/src/Pure/Isar/method.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/Pure/Isar/method.ML	Mon May 02 16:33:21 2011 +0200
@@ -218,7 +218,7 @@
 
 (* rule etc. -- single-step refinements *)
 
-val (rule_trace, rule_trace_setup) = Attrib.config_bool "rule_trace" (fn _ => false);
+val rule_trace = Attrib.setup_config_bool (Binding.name "rule_trace") (fn _ => false);
 
 fun trace ctxt rules =
   if Config.get ctxt rule_trace andalso not (null rules) then
@@ -441,8 +441,7 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (rule_trace_setup #>
-  setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
+ (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
   setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
   setup (Binding.name "-") (Scan.succeed (K insert_facts))
     "do nothing (insert current facts only)" #>

--- a/src/Pure/Thy/thy_output.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon May 02 16:33:21 2011 +0200
@@ -51,14 +51,11 @@
 val source_default = Unsynchronized.ref false;
 val break_default = Unsynchronized.ref false;
 
-val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default);
-val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default);
-val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default);
-val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default);
-val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default);
-
-val _ = Context.>> (Context.map_theory
- (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break));
+val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default);
+val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default);
+val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default);
+val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default);
+val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default);
 
 
 structure Wrappers = Proof_Data

--- a/src/Tools/quickcheck.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon May 02 16:33:21 2011 +0200
@@ -132,21 +132,16 @@
   if expect1 = expect2 then expect1 else No_Expectation
 
 (* quickcheck configuration -- default parameters, test generators *)
-val (tester, setup_tester) = Attrib.config_string "quickcheck_tester" (K "")
-val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
-val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
-val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
-val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
-val (timing, setup_timing) = Attrib.config_bool "quickcheck_timing" (K false)
-val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
-val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
-val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
-val (finite_type_size, setup_finite_type_size) =
-  Attrib.config_int "quickcheck_finite_type_size" (K 3)
-
-val setup_config =
-  setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_timing
-    #> setup_quiet #> setup_timeout #> setup_finite_types #> setup_finite_type_size
+val tester = Attrib.setup_config_string @{binding quickcheck_tester} (K "")
+val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
+val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
+val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
+val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
+val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
+val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
+val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
+val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3)
 
 datatype test_params = Test_Params of
   {default_type: typ list, expect : expectation};
@@ -536,7 +531,6 @@
   end
 
 val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
-  #> setup_config
 
 (* Isar commands *)
 

--- a/src/Tools/subtyping.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/Tools/subtyping.ML	Mon May 02 16:33:21 2011 +0200
@@ -711,8 +711,7 @@
 
 (* term check *)
 
-val (coercion_enabled, coercion_enabled_setup) =
-  Attrib.config_bool "coercion_enabled" (K false);
+val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
 
 val add_term_check =
   Syntax.add_term_check ~100 "coercions"
@@ -820,7 +819,6 @@
 (* theory setup *)
 
 val setup =
-  coercion_enabled_setup #>
   Context.theory_map add_term_check #>
   Attrib.setup @{binding coercion}
     (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))