1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Mon May 02 13:29:47 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon May 02 16:33:21 2011 +0200
     1.3 @@ -593,14 +593,14 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\
     1.6    @{index_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\
     1.7 -  @{index_ML Attrib.config_bool: "string -> (Context.generic -> bool) ->
     1.8 -  bool Config.T * (theory -> theory)"} \\
     1.9 -  @{index_ML Attrib.config_int: "string -> (Context.generic -> int) ->
    1.10 -  int Config.T * (theory -> theory)"} \\
    1.11 -  @{index_ML Attrib.config_real: "string -> (Context.generic -> real) ->
    1.12 -  real Config.T * (theory -> theory)"} \\
    1.13 -  @{index_ML Attrib.config_string: "string -> (Context.generic -> string) ->
    1.14 -  string Config.T * (theory -> theory)"} \\
    1.15 +  @{index_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) ->
    1.16 +  bool Config.T"} \\
    1.17 +  @{index_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) ->
    1.18 +  int Config.T"} \\
    1.19 +  @{index_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) ->
    1.20 +  real Config.T"} \\
    1.21 +  @{index_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) ->
    1.22 +  string Config.T"} \\
    1.23    \end{mldecls}
    1.24  
    1.25    \begin{description}
    1.26 @@ -611,13 +611,13 @@
    1.27    \item @{ML Config.map}~@{text "config f ctxt"} updates the context
    1.28    by updating the value of @{text "config"}.
    1.29  
    1.30 -  \item @{text "(config, setup) ="}~@{ML Attrib.config_bool}~@{text
    1.31 -  "name default"} creates a named configuration option of type
    1.32 -  @{ML_type bool}, with the given @{text "default"} depending on the
    1.33 -  application context.  The resulting @{text "config"} can be used to
    1.34 -  get/map its value in a given context.  The @{text "setup"} function
    1.35 -  needs to be applied to the theory initially, in order to make
    1.36 -  concrete declaration syntax available to the user.
    1.37 +  \item @{text "config ="}~@{ML Attrib.setup_config_bool}~@{text "name
    1.38 +  default"} creates a named configuration option of type @{ML_type
    1.39 +  bool}, with the given @{text "default"} depending on the application
    1.40 +  context.  The resulting @{text "config"} can be used to get/map its
    1.41 +  value in a given context.  There is an implicit update of the
    1.42 +  background theory that registers the option as attribute with some
    1.43 +  concrete syntax.
    1.44  
    1.45    \item @{ML Attrib.config_int}, @{ML Attrib.config_real}, and @{ML
    1.46    Attrib.config_string} work like @{ML Attrib.config_bool}, but for
    1.47 @@ -631,10 +631,9 @@
    1.48    default value @{ML false}.  *}
    1.49  
    1.50  ML {*
    1.51 -  val (my_flag, my_flag_setup) =
    1.52 -    Attrib.config_bool "my_flag" (K false)
    1.53 +  val my_flag =
    1.54 +    Attrib.setup_config_bool @{binding my_flag} (K false)
    1.55  *}
    1.56 -setup my_flag_setup
    1.57  
    1.58  text {* Now the user can refer to @{attribute my_flag} in
    1.59    declarations, while ML tools can retrieve the current value from the
    1.60 @@ -659,10 +658,9 @@
    1.61    (floating-point numbers). *}
    1.62  
    1.63  ML {*
    1.64 -  val (airspeed_velocity, airspeed_velocity_setup) =
    1.65 -    Attrib.config_real "airspeed_velocity" (K 0.0)
    1.66 +  val airspeed_velocity =
    1.67 +    Attrib.setup_config_real @{binding airspeed_velocity} (K 0.0)
    1.68  *}
    1.69 -setup airspeed_velocity_setup
    1.70  
    1.71  declare [[airspeed_velocity = 10]]
    1.72  declare [[airspeed_velocity = 9.9]]

     2.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon May 02 13:29:47 2011 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon May 02 16:33:21 2011 +0200
     2.3 @@ -797,14 +797,14 @@
     2.4  \begin{mldecls}
     2.5    \indexdef{}{ML}{Config.get}\verb|Config.get: Proof.context -> 'a Config.T -> 'a| \\
     2.6    \indexdef{}{ML}{Config.map}\verb|Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context| \\
     2.7 -  \indexdef{}{ML}{Attrib.config\_bool}\verb|Attrib.config_bool: string -> (Context.generic -> bool) ->|\isasep\isanewline%
     2.8 -\verb|  bool Config.T * (theory -> theory)| \\
     2.9 -  \indexdef{}{ML}{Attrib.config\_int}\verb|Attrib.config_int: string -> (Context.generic -> int) ->|\isasep\isanewline%
    2.10 -\verb|  int Config.T * (theory -> theory)| \\
    2.11 -  \indexdef{}{ML}{Attrib.config\_real}\verb|Attrib.config_real: string -> (Context.generic -> real) ->|\isasep\isanewline%
    2.12 -\verb|  real Config.T * (theory -> theory)| \\
    2.13 -  \indexdef{}{ML}{Attrib.config\_string}\verb|Attrib.config_string: string -> (Context.generic -> string) ->|\isasep\isanewline%
    2.14 -\verb|  string Config.T * (theory -> theory)| \\
    2.15 +  \indexdef{}{ML}{Attrib.setup\_config\_bool}\verb|Attrib.setup_config_bool: binding -> (Context.generic -> bool) ->|\isasep\isanewline%
    2.16 +\verb|  bool Config.T| \\
    2.17 +  \indexdef{}{ML}{Attrib.setup\_config\_int}\verb|Attrib.setup_config_int: binding -> (Context.generic -> int) ->|\isasep\isanewline%
    2.18 +\verb|  int Config.T| \\
    2.19 +  \indexdef{}{ML}{Attrib.setup\_config\_real}\verb|Attrib.setup_config_real: binding -> (Context.generic -> real) ->|\isasep\isanewline%
    2.20 +\verb|  real Config.T| \\
    2.21 +  \indexdef{}{ML}{Attrib.setup\_config\_string}\verb|Attrib.setup_config_string: binding -> (Context.generic -> string) ->|\isasep\isanewline%
    2.22 +\verb|  string Config.T| \\
    2.23    \end{mldecls}
    2.24  
    2.25    \begin{description}
    2.26 @@ -815,12 +815,11 @@
    2.27    \item \verb|Config.map|~\isa{config\ f\ ctxt} updates the context
    2.28    by updating the value of \isa{config}.
    2.29  
    2.30 -  \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
    2.31 -  \verb|bool|, with the given \isa{default} depending on the
    2.32 -  application context.  The resulting \isa{config} can be used to
    2.33 -  get/map its value in a given context.  The \isa{setup} function
    2.34 -  needs to be applied to the theory initially, in order to make
    2.35 -  concrete declaration syntax available to the user.
    2.36 +  \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
    2.37 +  context.  The resulting \isa{config} can be used to get/map its
    2.38 +  value in a given context.  There is an implicit update of the
    2.39 +  background theory that registers the option as attribute with some
    2.40 +  concrete syntax.
    2.41  
    2.42    \item \verb|Attrib.config_int|, \verb|Attrib.config_real|, and \verb|Attrib.config_string| work like \verb|Attrib.config_bool|, but for
    2.43    types \verb|int| and \verb|string|, respectively.
    2.44 @@ -863,11 +862,13 @@
    2.45  \isatagML
    2.46  \isacommand{ML}\isamarkupfalse%
    2.47  \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
    2.48 -\ \ 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
    2.49 -\ \ \ \ 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
    2.50 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
    2.51 -\isacommand{setup}\isamarkupfalse%
    2.52 -\ my{\isaliteral{5F}{\isacharunderscore}}flag{\isaliteral{5F}{\isacharunderscore}}setup%
    2.53 +\ \ val\ my{\isaliteral{5F}{\isacharunderscore}}flag\ {\isaliteral{3D}{\isacharequal}}\isanewline
    2.54 +\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}bool\ %
    2.55 +\isaantiq
    2.56 +binding\ my{\isaliteral{5F}{\isacharunderscore}}flag{}%
    2.57 +\endisaantiq
    2.58 +\ {\isaliteral{28}{\isacharparenleft}}K\ false{\isaliteral{29}{\isacharparenright}}\isanewline
    2.59 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
    2.60  \endisatagML
    2.61  {\isafoldML}%
    2.62  %
    2.63 @@ -1028,11 +1029,13 @@
    2.64  \isatagML
    2.65  \isacommand{ML}\isamarkupfalse%
    2.66  \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
    2.67 -\ \ 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
    2.68 -\ \ \ \ 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
    2.69 -{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
    2.70 -\isacommand{setup}\isamarkupfalse%
    2.71 -\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{\isaliteral{5F}{\isacharunderscore}}setup%
    2.72 +\ \ val\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity\ {\isaliteral{3D}{\isacharequal}}\isanewline
    2.73 +\ \ \ \ Attrib{\isaliteral{2E}{\isachardot}}setup{\isaliteral{5F}{\isacharunderscore}}config{\isaliteral{5F}{\isacharunderscore}}real\ %
    2.74 +\isaantiq
    2.75 +binding\ airspeed{\isaliteral{5F}{\isacharunderscore}}velocity{}%
    2.76 +\endisaantiq
    2.77 +\ {\isaliteral{28}{\isacharparenleft}}K\ {\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
    2.78 +{\isaliteral{2A7D}{\isacharverbatimclose}}%
    2.79  \endisatagML
    2.80  {\isafoldML}%
    2.81  %

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

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

     5.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon May 02 13:29:47 2011 +0200
     5.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon May 02 16:33:21 2011 +0200
     5.3 @@ -24,7 +24,7 @@
     5.4  
     5.5  (*** calling provers ***)
     5.6  
     5.7 -val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "")
     5.8 +val dest_dir = Attrib.setup_config_string @{binding sos_dest_dir} (K "")
     5.9  
    5.10  fun filename dir name =
    5.11    let
    5.12 @@ -117,7 +117,7 @@
    5.13    | prover "csdp" = csdp
    5.14    | prover name = error ("Unknown prover: " ^ name)
    5.15  
    5.16 -val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp")
    5.17 +val prover_name = Attrib.setup_config_string @{binding sos_prover_name} (K "remote_csdp")
    5.18  
    5.19  fun call_solver ctxt opt_name =
    5.20    let
    5.21 @@ -140,8 +140,6 @@
    5.22  fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method
    5.23  
    5.24  val setup =
    5.25 -  setup_dest_dir #>
    5.26 -  setup_prover_name #>
    5.27    Method.setup @{binding sos}
    5.28      (Scan.lift (Scan.option Parse.xname)
    5.29        >> (fn opt_name => fn ctxt =>

     6.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon May 02 13:29:47 2011 +0200
     6.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon May 02 16:33:21 2011 +0200
     6.3 @@ -10,7 +10,6 @@
     6.4    datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
     6.5    val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
     6.6    val trace: bool Config.T
     6.7 -  val setup: theory -> theory
     6.8    exception Failure of string;
     6.9  end
    6.10  
    6.11 @@ -50,8 +49,7 @@
    6.12  val pow2 = rat_pow rat_2;
    6.13  val pow10 = rat_pow rat_10;
    6.14  
    6.15 -val (trace, setup_trace) = Attrib.config_bool "sos_trace" (K false);
    6.16 -val setup = setup_trace;
    6.17 +val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
    6.18  
    6.19  exception Sanity;
    6.20  

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

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

     9.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Mon May 02 13:29:47 2011 +0200
     9.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Mon May 02 16:33:21 2011 +0200
     9.3 @@ -14,8 +14,6 @@
     9.4  
     9.5  ML {* Toplevel.add_hook Mirabelle.step_hook *}
     9.6  
     9.7 -setup Mirabelle.setup
     9.8 -
     9.9  ML {*
    9.10  signature MIRABELLE_ACTION =
    9.11  sig

    10.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 02 13:29:47 2011 +0200
    10.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 02 16:33:21 2011 +0200
    10.3 @@ -9,7 +9,6 @@
    10.4    val timeout : int Config.T
    10.5    val start_line : int Config.T
    10.6    val end_line : int Config.T
    10.7 -  val setup : theory -> theory
    10.8  
    10.9    (*core*)
   10.10    type init_action = int -> theory -> theory
   10.11 @@ -43,12 +42,10 @@
   10.12  
   10.13  (* Mirabelle configuration *)
   10.14  
   10.15 -val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" (K "")
   10.16 -val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" (K 30)
   10.17 -val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" (K 0)
   10.18 -val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" (K ~1)
   10.19 -
   10.20 -val setup = setup1 #> setup2 #> setup3 #> setup4
   10.21 +val logfile = Attrib.setup_config_string @{binding mirabelle_logfile} (K "")
   10.22 +val timeout = Attrib.setup_config_int @{binding mirabelle_timeout} (K 30)
   10.23 +val start_line = Attrib.setup_config_int @{binding mirabelle_start_line} (K 0)
   10.24 +val end_line = Attrib.setup_config_int @{binding mirabelle_end_line} (K ~1)
   10.25  
   10.26  
   10.27  (* Mirabelle core *)

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

    12.1 --- a/src/HOL/Sledgehammer.thy	Mon May 02 13:29:47 2011 +0200
    12.2 +++ b/src/HOL/Sledgehammer.thy	Mon May 02 16:33:21 2011 +0200
    12.3 @@ -19,9 +19,6 @@
    12.4       "Tools/Sledgehammer/sledgehammer_isar.ML"
    12.5  begin
    12.6  
    12.7 -setup {*
    12.8 -  Sledgehammer_Provers.setup
    12.9 -  #> Sledgehammer_Isar.setup
   12.10 -*}
   12.11 +setup {* Sledgehammer_Isar.setup *}
   12.12  
   12.13  end

    13.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon May 02 13:29:47 2011 +0200
    13.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon May 02 16:33:21 2011 +0200
    13.3 @@ -40,19 +40,17 @@
    13.4    val make_meta_clause: thm -> thm
    13.5    val make_meta_clauses: thm list -> thm list
    13.6    val meson_tac: Proof.context -> thm list -> int -> tactic
    13.7 -  val setup : theory -> theory
    13.8  end
    13.9  
   13.10  structure Meson : MESON =
   13.11  struct
   13.12  
   13.13 -val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
   13.14 +val trace = Attrib.setup_config_bool @{binding meson_trace} (K false)
   13.15  
   13.16  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
   13.17  
   13.18  val max_clauses_default = 60
   13.19 -val (max_clauses, max_clauses_setup) =
   13.20 -  Attrib.config_int "meson_max_clauses" (K max_clauses_default)
   13.21 +val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K max_clauses_default)
   13.22  
   13.23  (*No known example (on 1-5-2007) needs even thirty*)
   13.24  val iter_deepen_limit = 50;
   13.25 @@ -738,8 +736,4 @@
   13.26      name_thms "MClause#"
   13.27        (distinct Thm.eq_thm_prop (map make_meta_clause ths));
   13.28  
   13.29 -val setup =
   13.30 -  trace_setup
   13.31 -  #> max_clauses_setup
   13.32 -
   13.33  end;

    14.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 02 13:29:47 2011 +0200
    14.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 02 16:33:21 2011 +0200
    14.3 @@ -23,7 +23,6 @@
    14.4      -> (Metis_Thm.thm * thm) list
    14.5    val discharge_skolem_premises :
    14.6      Proof.context -> (thm * term) option list -> thm -> thm
    14.7 -  val setup : theory -> theory
    14.8  end;
    14.9  
   14.10  structure Metis_Reconstruct : METIS_RECONSTRUCT =
   14.11 @@ -31,8 +30,8 @@
   14.12  
   14.13  open Metis_Translate
   14.14  
   14.15 -val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
   14.16 -val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
   14.17 +val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
   14.18 +val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
   14.19  
   14.20  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
   14.21  fun verbose_warning ctxt msg =
   14.22 @@ -897,6 +896,4 @@
   14.23                      \Error when discharging Skolem assumptions.")
   14.24      end
   14.25  
   14.26 -val setup = trace_setup #> verbose_setup
   14.27 -
   14.28  end;

    15.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 02 13:29:47 2011 +0200
    15.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 02 16:33:21 2011 +0200
    15.3 @@ -25,9 +25,8 @@
    15.4  open Metis_Translate
    15.5  open Metis_Reconstruct
    15.6  
    15.7 -val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
    15.8 -val (new_skolemizer, new_skolemizer_setup) =
    15.9 -  Attrib.config_bool "metis_new_skolemizer" (K false)
   15.10 +val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
   15.11 +val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
   15.12  
   15.13  fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   15.14  
   15.15 @@ -190,9 +189,7 @@
   15.16                 end)))
   15.17  
   15.18  val setup =
   15.19 -  type_lits_setup
   15.20 -  #> new_skolemizer_setup
   15.21 -  #> method @{binding metis} HO "Metis for FOL/HOL problems"
   15.22 +  method @{binding metis} HO "Metis for FOL/HOL problems"
   15.23    #> method @{binding metisF} FO "Metis for FOL problems"
   15.24    #> method @{binding metisFT} FT
   15.25              "Metis for FOL/HOL problems with fully-typed translation"

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

    17.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon May 02 13:29:47 2011 +0200
    17.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon May 02 16:33:21 2011 +0200
    17.3 @@ -28,20 +28,11 @@
    17.4  
    17.5  (** dynamic options **)
    17.6  
    17.7 -val (smart_quantifier, setup_smart_quantifier) =
    17.8 -  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    17.9 -
   17.10 -val (fast, setup_fast) =
   17.11 -  Attrib.config_bool "quickcheck_fast" (K false)
   17.12 -
   17.13 -val (bounded_forall, setup_bounded_forall) =
   17.14 -  Attrib.config_bool "quickcheck_bounded_forall" (K false)
   17.15 -  
   17.16 -val (full_support, setup_full_support) =
   17.17 -  Attrib.config_bool "quickcheck_full_support" (K true)
   17.18 -
   17.19 -val (quickcheck_pretty, setup_quickcheck_pretty) =
   17.20 -  Attrib.config_bool "quickcheck_pretty" (K true)
   17.21 +val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
   17.22 +val fast = Attrib.setup_config_bool @{binding quickcheck_fast} (K false)
   17.23 +val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false)
   17.24 +val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
   17.25 +val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
   17.26   
   17.27  (** general term functions **)
   17.28  
   17.29 @@ -508,11 +499,6 @@
   17.30        (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
   17.31    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   17.32        (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
   17.33 -  #> setup_smart_quantifier
   17.34 -  #> setup_full_support
   17.35 -  #> setup_fast
   17.36 -  #> setup_bounded_forall
   17.37 -  #> setup_quickcheck_pretty
   17.38    #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   17.39    #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   17.40    #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));

    18.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 02 13:29:47 2011 +0200
    18.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 02 16:33:21 2011 +0200
    18.3 @@ -18,8 +18,7 @@
    18.4  
    18.5  (* configurations *)
    18.6  
    18.7 -val (finite_functions, setup_finite_functions) =
    18.8 -  Attrib.config_bool "quickcheck_finite_functions" (K true)
    18.9 +val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
   18.10  
   18.11  (* narrowing specific names and types *)
   18.12  
   18.13 @@ -208,7 +207,6 @@
   18.14  val setup =
   18.15    Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   18.16      (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
   18.17 -  #> setup_finite_functions
   18.18    #> Context.theory_map
   18.19      (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   18.20      

    19.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon May 02 13:29:47 2011 +0200
    19.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon May 02 16:33:21 2011 +0200
    19.3 @@ -23,12 +23,10 @@
    19.4    (*options*)
    19.5    val oracle: bool Config.T
    19.6    val datatypes: bool Config.T
    19.7 -  val timeoutN: string
    19.8    val timeout: real Config.T
    19.9    val random_seed: int Config.T
   19.10    val fixed: bool Config.T
   19.11    val verbose: bool Config.T
   19.12 -  val traceN: string
   19.13    val trace: bool Config.T
   19.14    val trace_used_facts: bool Config.T
   19.15    val monomorph_limit: int Config.T
   19.16 @@ -149,75 +147,21 @@
   19.17  
   19.18  (* options *)
   19.19  
   19.20 -val oracleN = "smt_oracle"
   19.21 -val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
   19.22 -
   19.23 -val datatypesN = "smt_datatypes"
   19.24 -val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
   19.25 -
   19.26 -val timeoutN = "smt_timeout"
   19.27 -val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
   19.28 -
   19.29 -val random_seedN = "smt_random_seed"
   19.30 -val (random_seed, setup_random_seed) = Attrib.config_int random_seedN (K 1)
   19.31 -
   19.32 -val fixedN = "smt_fixed"
   19.33 -val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
   19.34 -
   19.35 -val verboseN = "smt_verbose"
   19.36 -val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
   19.37 -
   19.38 -val traceN = "smt_trace"
   19.39 -val (trace, setup_trace) = Attrib.config_bool traceN (K false)
   19.40 -
   19.41 -val trace_used_factsN = "smt_trace_used_facts"
   19.42 -val (trace_used_facts, setup_trace_used_facts) =
   19.43 -  Attrib.config_bool trace_used_factsN (K false)
   19.44 -
   19.45 -val monomorph_limitN = "smt_monomorph_limit"
   19.46 -val (monomorph_limit, setup_monomorph_limit) =
   19.47 -  Attrib.config_int monomorph_limitN (K 10)
   19.48 -
   19.49 -val monomorph_instancesN = "smt_monomorph_instances"
   19.50 -val (monomorph_instances, setup_monomorph_instances) =
   19.51 -  Attrib.config_int monomorph_instancesN (K 500)
   19.52 -
   19.53 -val monomorph_fullN = "smt_monomorph_full"
   19.54 -val (monomorph_full, setup_monomorph_full) =
   19.55 -  Attrib.config_bool monomorph_fullN (K true)
   19.56 -
   19.57 -val infer_triggersN = "smt_infer_triggers"
   19.58 -val (infer_triggers, setup_infer_triggers) =
   19.59 -  Attrib.config_bool infer_triggersN (K false)
   19.60 -
   19.61 -val drop_bad_factsN = "smt_drop_bad_facts"
   19.62 -val (drop_bad_facts, setup_drop_bad_facts) =
   19.63 -  Attrib.config_bool drop_bad_factsN (K false)
   19.64 -
   19.65 -val filter_only_factsN = "smt_filter_only_facts"
   19.66 -val (filter_only_facts, setup_filter_only_facts) =
   19.67 -  Attrib.config_bool filter_only_factsN (K false)
   19.68 -
   19.69 -val debug_filesN = "smt_debug_files"
   19.70 -val (debug_files, setup_debug_files) =
   19.71 -  Attrib.config_string debug_filesN (K "")
   19.72 -
   19.73 -val setup_options =
   19.74 -  setup_oracle #>
   19.75 -  setup_datatypes #>
   19.76 -  setup_timeout #>
   19.77 -  setup_random_seed #>
   19.78 -  setup_fixed #>
   19.79 -  setup_trace #>
   19.80 -  setup_verbose #>
   19.81 -  setup_monomorph_limit #>
   19.82 -  setup_monomorph_instances #>
   19.83 -  setup_monomorph_full #>
   19.84 -  setup_infer_triggers #>
   19.85 -  setup_drop_bad_facts #>
   19.86 -  setup_filter_only_facts #>
   19.87 -  setup_trace_used_facts #>
   19.88 -  setup_debug_files
   19.89 +val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
   19.90 +val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false)
   19.91 +val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
   19.92 +val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
   19.93 +val fixed = Attrib.setup_config_bool @{binding smt_fixed} (K false)
   19.94 +val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
   19.95 +val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
   19.96 +val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
   19.97 +val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
   19.98 +val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
   19.99 +val monomorph_full = Attrib.setup_config_bool @{binding smt_monomorph_full} (K true)
  19.100 +val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
  19.101 +val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
  19.102 +val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
  19.103 +val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
  19.104  
  19.105  
  19.106  (* diagnostics *)
  19.107 @@ -269,7 +213,6 @@
  19.108  
  19.109  val setup =
  19.110    setup_solver #>
  19.111 -  setup_options #>
  19.112    setup_certificates
  19.113  
  19.114  fun print_setup ctxt =

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

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

    22.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 13:29:47 2011 +0200
    22.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 16:33:21 2011 +0200
    22.3 @@ -96,7 +96,6 @@
    22.4    val running_provers : unit -> unit
    22.5    val messages : int option -> unit
    22.6    val get_prover : Proof.context -> bool -> string -> prover
    22.7 -  val setup : theory -> theory
    22.8  end;
    22.9  
   22.10  structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
   22.11 @@ -272,15 +271,15 @@
   22.12  
   22.13  (* configuration attributes *)
   22.14  
   22.15 -val (dest_dir, dest_dir_setup) =
   22.16 -  Attrib.config_string "sledgehammer_dest_dir" (K "")
   22.17 +val dest_dir =
   22.18 +  Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
   22.19    (* Empty string means create files in Isabelle's temporary files directory. *)
   22.20  
   22.21 -val (problem_prefix, problem_prefix_setup) =
   22.22 -  Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
   22.23 +val problem_prefix =
   22.24 +  Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
   22.25  
   22.26 -val (measure_run_time, measure_run_time_setup) =
   22.27 -  Attrib.config_bool "sledgehammer_measure_run_time" (K false)
   22.28 +val measure_run_time =
   22.29 +  Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
   22.30  
   22.31  fun with_path cleanup after f path =
   22.32    Exn.capture f path
   22.33 @@ -806,9 +805,4 @@
   22.34        error ("No such prover: " ^ name ^ ".")
   22.35    end
   22.36  
   22.37 -val setup =
   22.38 -  dest_dir_setup
   22.39 -  #> problem_prefix_setup
   22.40 -  #> measure_run_time_setup
   22.41 -
   22.42  end;

    23.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon May 02 13:29:47 2011 +0200
    23.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 02 16:33:21 2011 +0200
    23.3 @@ -862,10 +862,10 @@
    23.4        NONE => deepen bound f (i + 1)
    23.5      | SOME x => SOME x);
    23.6  
    23.7 -val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" (K 10);
    23.8 -val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" (K 1);
    23.9 -val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
   23.10 -val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
   23.11 +val depth_bound = Attrib.setup_config_int @{binding ind_quickcheck_depth} (K 10);
   23.12 +val depth_start = Attrib.setup_config_int @{binding ind_quickcheck_depth_start} (K 1);
   23.13 +val random_values = Attrib.setup_config_int @{binding ind_quickcheck_random} (K 5);
   23.14 +val size_offset = Attrib.setup_config_int @{binding ind_quickcheck_size_offset} (K 0);
   23.15  
   23.16  fun test_term ctxt [(t, [])] =
   23.17        let
   23.18 @@ -925,10 +925,6 @@
   23.19        error "Compilation of multiple instances is not supported by tester SML_inductive";
   23.20  
   23.21  val quickcheck_setup =
   23.22 -  setup_depth_bound #>
   23.23 -  setup_depth_start #>
   23.24 -  setup_random_values #>
   23.25 -  setup_size_offset #>
   23.26    Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
   23.27  
   23.28  end;

    24.1 --- a/src/HOL/Tools/lin_arith.ML	Mon May 02 13:29:47 2011 +0200
    24.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon May 02 16:33:21 2011 +0200
    24.3 @@ -99,8 +99,8 @@
    24.4    {splits = splits, inj_consts = update (op =) c inj_consts,
    24.5     discrete = discrete});
    24.6  
    24.7 -val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" (K 9);
    24.8 -val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" (K 9);
    24.9 +val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
   24.10 +val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
   24.11  
   24.12  
   24.13  structure LA_Data =
   24.14 @@ -905,7 +905,6 @@
   24.15        (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
   24.16  
   24.17  val global_setup =
   24.18 -  setup_split_limit #> setup_neq_limit #>
   24.19    Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
   24.20      "declaration of split rules for arithmetic procedure" #>
   24.21    Method.setup @{binding linarith}

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

    26.1 --- a/src/Pure/Isar/attrib.ML	Mon May 02 13:29:47 2011 +0200
    26.2 +++ b/src/Pure/Isar/attrib.ML	Mon May 02 16:33:21 2011 +0200
    26.3 @@ -36,15 +36,26 @@
    26.4    val multi_thm: thm list context_parser
    26.5    val print_configs: Proof.context -> unit
    26.6    val internal: (morphism -> attribute) -> src
    26.7 -  val config_bool: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    26.8 -  val config_int: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
    26.9 -  val config_real: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
   26.10 -  val config_string: bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
   26.11 -  val config_bool_global: bstring -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   26.12 -  val config_int_global: bstring -> (Context.generic -> int) -> int Config.T * (theory -> theory)
   26.13 -  val config_real_global: bstring -> (Context.generic -> real) -> real Config.T * (theory -> theory)
   26.14 -  val config_string_global:
   26.15 -    bstring -> (Context.generic -> string) -> string Config.T * (theory -> theory)
   26.16 +  val config_bool: Binding.binding ->
   26.17 +    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   26.18 +  val config_int: Binding.binding ->
   26.19 +    (Context.generic -> int) -> int Config.T * (theory -> theory)
   26.20 +  val config_real: Binding.binding ->
   26.21 +    (Context.generic -> real) -> real Config.T * (theory -> theory)
   26.22 +  val config_string: Binding.binding ->
   26.23 +    (Context.generic -> string) -> string Config.T * (theory -> theory)
   26.24 +  val config_bool_global: Binding.binding ->
   26.25 +    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
   26.26 +  val config_int_global: Binding.binding ->
   26.27 +    (Context.generic -> int) -> int Config.T * (theory -> theory)
   26.28 +  val config_real_global: Binding.binding ->
   26.29 +    (Context.generic -> real) -> real Config.T * (theory -> theory)
   26.30 +  val config_string_global: Binding.binding ->
   26.31 +    (Context.generic -> string) -> string Config.T * (theory -> theory)
   26.32 +  val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
   26.33 +  val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
   26.34 +  val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
   26.35 +  val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
   26.36  end;
   26.37  
   26.38  structure Attrib: ATTRIB =
   26.39 @@ -366,34 +377,53 @@
   26.40    let val config_type = Config.get_global thy config
   26.41    in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
   26.42  
   26.43 -in
   26.44 -
   26.45 -fun register_config config thy =
   26.46 -  let
   26.47 -    val bname = Config.name_of config;
   26.48 -    val name = Sign.full_bname thy bname;
   26.49 -  in
   26.50 +fun register binding config thy =
   26.51 +  let val name = Sign.full_name thy binding in
   26.52      thy
   26.53 -    |> setup (Binding.name bname) (Scan.lift (scan_config thy config) >> Morphism.form)
   26.54 -      "configuration option"
   26.55 +    |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option"
   26.56      |> Configs.map (Symtab.update (name, config))
   26.57    end;
   26.58  
   26.59 -fun declare_config make coerce global name default =
   26.60 +fun declare make coerce global binding default =
   26.61    let
   26.62 +    val name = Binding.name_of binding;
   26.63      val config_value = Config.declare_generic {global = global} name (make o default);
   26.64      val config = coerce config_value;
   26.65 -  in (config, register_config config_value) end;
   26.66 +  in (config, register binding config_value) end;
   26.67  
   26.68 -val config_bool = declare_config Config.Bool Config.bool false;
   26.69 -val config_int = declare_config Config.Int Config.int false;
   26.70 -val config_real = declare_config Config.Real Config.real false;
   26.71 -val config_string = declare_config Config.String Config.string false;
   26.72 +in
   26.73  
   26.74 -val config_bool_global = declare_config Config.Bool Config.bool true;
   26.75 -val config_int_global = declare_config Config.Int Config.int true;
   26.76 -val config_real_global = declare_config Config.Real Config.real true;
   26.77 -val config_string_global = declare_config Config.String Config.string true;
   26.78 +val config_bool = declare Config.Bool Config.bool false;
   26.79 +val config_int = declare Config.Int Config.int false;
   26.80 +val config_real = declare Config.Real Config.real false;
   26.81 +val config_string = declare Config.String Config.string false;
   26.82 +
   26.83 +val config_bool_global = declare Config.Bool Config.bool true;
   26.84 +val config_int_global = declare Config.Int Config.int true;
   26.85 +val config_real_global = declare Config.Real Config.real true;
   26.86 +val config_string_global = declare Config.String Config.string true;
   26.87 +
   26.88 +fun register_config config = register (Binding.name (Config.name_of config)) config;
   26.89 +
   26.90 +end;
   26.91 +
   26.92 +
   26.93 +(* implicit setup *)
   26.94 +
   26.95 +local
   26.96 +
   26.97 +fun setup_config declare_config binding default =
   26.98 +  let
   26.99 +    val (config, setup) = declare_config binding default;
  26.100 +    val _ = Context.>> (Context.map_theory setup);
  26.101 +  in config end;
  26.102 +
  26.103 +in
  26.104 +
  26.105 +val setup_config_bool = setup_config config_bool;
  26.106 +val setup_config_int = setup_config config_int;
  26.107 +val setup_config_string = setup_config config_string;
  26.108 +val setup_config_real = setup_config config_real;
  26.109  
  26.110  end;
  26.111  

    27.1 --- a/src/Pure/Isar/method.ML	Mon May 02 13:29:47 2011 +0200
    27.2 +++ b/src/Pure/Isar/method.ML	Mon May 02 16:33:21 2011 +0200
    27.3 @@ -218,7 +218,7 @@
    27.4  
    27.5  (* rule etc. -- single-step refinements *)
    27.6  
    27.7 -val (rule_trace, rule_trace_setup) = Attrib.config_bool "rule_trace" (fn _ => false);
    27.8 +val rule_trace = Attrib.setup_config_bool (Binding.name "rule_trace") (fn _ => false);
    27.9  
   27.10  fun trace ctxt rules =
   27.11    if Config.get ctxt rule_trace andalso not (null rules) then
   27.12 @@ -441,8 +441,7 @@
   27.13  (* theory setup *)
   27.14  
   27.15  val _ = Context.>> (Context.map_theory
   27.16 - (rule_trace_setup #>
   27.17 -  setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
   27.18 + (setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
   27.19    setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
   27.20    setup (Binding.name "-") (Scan.succeed (K insert_facts))
   27.21      "do nothing (insert current facts only)" #>

    28.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 02 13:29:47 2011 +0200
    28.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 02 16:33:21 2011 +0200
    28.3 @@ -51,14 +51,11 @@
    28.4  val source_default = Unsynchronized.ref false;
    28.5  val break_default = Unsynchronized.ref false;
    28.6  
    28.7 -val (display, setup_display) = Attrib.config_bool "thy_output_display" (fn _ => ! display_default);
    28.8 -val (quotes, setup_quotes) = Attrib.config_bool "thy_output_quotes" (fn _ => ! quotes_default);
    28.9 -val (indent, setup_indent) = Attrib.config_int "thy_output_indent" (fn _ => ! indent_default);
   28.10 -val (source, setup_source) = Attrib.config_bool "thy_output_source" (fn _ => ! source_default);
   28.11 -val (break, setup_break) = Attrib.config_bool "thy_output_break" (fn _ => ! break_default);
   28.12 -
   28.13 -val _ = Context.>> (Context.map_theory
   28.14 - (setup_display #> setup_quotes #> setup_indent #> setup_source #> setup_break));
   28.15 +val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default);
   28.16 +val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default);
   28.17 +val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default);
   28.18 +val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default);
   28.19 +val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default);
   28.20  
   28.21  
   28.22  structure Wrappers = Proof_Data

    29.1 --- a/src/Tools/quickcheck.ML	Mon May 02 13:29:47 2011 +0200
    29.2 +++ b/src/Tools/quickcheck.ML	Mon May 02 16:33:21 2011 +0200
    29.3 @@ -132,21 +132,16 @@
    29.4    if expect1 = expect2 then expect1 else No_Expectation
    29.5  
    29.6  (* quickcheck configuration -- default parameters, test generators *)
    29.7 -val (tester, setup_tester) = Attrib.config_string "quickcheck_tester" (K "")
    29.8 -val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
    29.9 -val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
   29.10 -val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
   29.11 -val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
   29.12 -val (timing, setup_timing) = Attrib.config_bool "quickcheck_timing" (K false)
   29.13 -val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
   29.14 -val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
   29.15 -val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
   29.16 -val (finite_type_size, setup_finite_type_size) =
   29.17 -  Attrib.config_int "quickcheck_finite_type_size" (K 3)
   29.18 -
   29.19 -val setup_config =
   29.20 -  setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_timing
   29.21 -    #> setup_quiet #> setup_timeout #> setup_finite_types #> setup_finite_type_size
   29.22 +val tester = Attrib.setup_config_string @{binding quickcheck_tester} (K "")
   29.23 +val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
   29.24 +val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
   29.25 +val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
   29.26 +val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
   29.27 +val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
   29.28 +val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
   29.29 +val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
   29.30 +val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
   29.31 +val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3)
   29.32  
   29.33  datatype test_params = Test_Params of
   29.34    {default_type: typ list, expect : expectation};
   29.35 @@ -536,7 +531,6 @@
   29.36    end
   29.37  
   29.38  val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
   29.39 -  #> setup_config
   29.40  
   29.41  (* Isar commands *)
   29.42  

    30.1 --- a/src/Tools/subtyping.ML	Mon May 02 13:29:47 2011 +0200
    30.2 +++ b/src/Tools/subtyping.ML	Mon May 02 16:33:21 2011 +0200
    30.3 @@ -711,8 +711,7 @@
    30.4  
    30.5  (* term check *)
    30.6  
    30.7 -val (coercion_enabled, coercion_enabled_setup) =
    30.8 -  Attrib.config_bool "coercion_enabled" (K false);
    30.9 +val coercion_enabled = Attrib.setup_config_bool @{binding coercion_enabled} (K false);
   30.10  
   30.11  val add_term_check =
   30.12    Syntax.add_term_check ~100 "coercions"
   30.13 @@ -820,7 +819,6 @@
   30.14  (* theory setup *)
   30.15  
   30.16  val setup =
   30.17 -  coercion_enabled_setup #>
   30.18    Context.theory_map add_term_check #>
   30.19    Attrib.setup @{binding coercion}
   30.20      (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))