# HG changeset patch # User wenzelm # Date 1304346801 -7200 # Node ID 92715b528e78829f52b253d6f9a0bc2aca261404 # Parent c8673078f9153a3eacec4e183e10464723eea389 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings; diff -r c8673078f915 -r 92715b528e78 doc-src/IsarImplementation/Thy/Prelim.thy --- 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]] diff -r c8673078f915 -r 92715b528e78 doc-src/IsarImplementation/Thy/document/Prelim.tex --- 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}% % diff -r c8673078f915 -r 92715b528e78 src/FOLP/IFOLP.thy --- 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 diff -r c8673078f915 -r 92715b528e78 src/HOL/Library/Sum_of_Squares.thy --- 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 *} diff -r c8673078f915 -r 92715b528e78 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- 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 => diff -r c8673078f915 -r 92715b528e78 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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; diff -r c8673078f915 -r 92715b528e78 src/HOL/Meson.thy --- 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 diff -r c8673078f915 -r 92715b528e78 src/HOL/Metis.thy --- 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 diff -r c8673078f915 -r 92715b528e78 src/HOL/Mirabelle/Mirabelle.thy --- 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 diff -r c8673078f915 -r 92715b528e78 src/HOL/Mirabelle/Tools/mirabelle.ML --- 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 *) diff -r c8673078f915 -r 92715b528e78 src/HOL/Nominal/nominal_thmdecls.ML --- 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) diff -r c8673078f915 -r 92715b528e78 src/HOL/Sledgehammer.thy --- 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 diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Meson/meson.ML --- 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; diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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; diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Metis/metis_tactics.ML --- 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" diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 *) diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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)); diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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)) diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/SMT/smt_config.ML --- 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 = diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/SMT/smt_setup_solvers.ML --- 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 = diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/SMT/smt_solver.ML --- 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 diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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; diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/inductive_codegen.ML --- 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; diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/lin_arith.ML --- 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} diff -r c8673078f915 -r 92715b528e78 src/Provers/blast.ML --- 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) diff -r c8673078f915 -r 92715b528e78 src/Pure/Isar/attrib.ML --- 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; diff -r c8673078f915 -r 92715b528e78 src/Pure/Isar/method.ML --- 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)" #> diff -r c8673078f915 -r 92715b528e78 src/Pure/Thy/thy_output.ML --- 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 diff -r c8673078f915 -r 92715b528e78 src/Tools/quickcheck.ML --- 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 *) diff -r c8673078f915 -r 92715b528e78 src/Tools/subtyping.ML --- 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))))