--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Mar 28 16:59:06 2010 +0200
@@ -43,10 +43,10 @@
(* Mirabelle configuration *)
-val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
-val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
-val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
-val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
+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
--- a/src/HOL/SMT/Tools/smt_normalize.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Sun Mar 28 16:59:06 2010 +0200
@@ -290,7 +290,7 @@
(* include additional rules *)
val (unfold_defs, unfold_defs_setup) =
- Attrib.config_bool "smt_unfold_defs" true
+ Attrib.config_bool "smt_unfold_defs" (K true)
local
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
--- a/src/HOL/SMT/Tools/smt_solver.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Sun Mar 28 16:59:06 2010 +0200
@@ -79,13 +79,13 @@
(* SMT options *)
-val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" 30
+val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
fun with_timeout ctxt f x =
TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
handle TimeLimit.TimeOut => raise SMT "timeout"
-val (trace, setup_trace) = Attrib.config_bool "smt_trace" false
+val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false)
fun trace_msg ctxt f x =
if Config.get ctxt trace then tracing (f x) else ()
@@ -93,7 +93,7 @@
(* SMT certificates *)
-val (record, setup_record) = Attrib.config_bool "smt_record" true
+val (record, setup_record) = Attrib.config_bool "smt_record" (K true)
structure Certificates = Generic_Data
(
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Sun Mar 28 16:59:06 2010 +0200
@@ -476,7 +476,7 @@
val true_false = @{lemma "True == ~ False" by simp}
val (trace_assms, trace_assms_setup) =
- Attrib.config_bool "z3_trace_assms" false
+ Attrib.config_bool "z3_trace_assms" (K false)
local
val TT_eq = @{lemma "(P = (~False)) == P" by simp}
--- a/src/HOL/SMT/Tools/z3_solver.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_solver.ML Sun Mar 28 16:59:06 2010 +0200
@@ -17,8 +17,8 @@
val solver_name = "z3"
val env_var = "Z3_SOLVER"
-val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" false
-val (options, options_setup) = Attrib.config_string "z3_options" ""
+val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
+val (options, options_setup) = Attrib.config_string "z3_options" (K "")
fun add xs ys = ys @ xs
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sun Mar 28 16:59:06 2010 +0200
@@ -30,14 +30,14 @@
(* external problem files *)
-val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" "";
+val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" (K "");
(*Empty string means create files in Isabelle's temporary files directory.*)
val (problem_prefix, problem_prefix_setup) =
- Attrib.config_string "atp_problem_prefix" "prob";
+ Attrib.config_string "atp_problem_prefix" (K "prob");
val (measure_runtime, measure_runtime_setup) =
- Attrib.config_bool "atp_measure_runtime" false;
+ Attrib.config_bool "atp_measure_runtime" (K false);
(* prover configuration *)
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sun Mar 28 16:59:06 2010 +0200
@@ -27,7 +27,7 @@
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
-val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
+val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Mar 28 16:59:06 2010 +0200
@@ -34,10 +34,10 @@
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
(*For generating structured proofs: keep every nth proof line*)
-val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;
+val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" (K 1);
(*Indicates whether to include sort information in generated proofs*)
-val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
+val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" (K true);
val setup = modulus_setup #> recon_sorts_setup;
--- a/src/HOL/Tools/inductive_codegen.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Sun Mar 28 16:59:06 2010 +0200
@@ -794,10 +794,10 @@
NONE => deepen bound f (i + 1)
| SOME x => SOME x);
-val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" 10;
-val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" 1;
-val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" 5;
-val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" 0;
+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);
fun test_term ctxt report t =
let
--- a/src/HOL/Tools/lin_arith.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sun Mar 28 16:59:06 2010 +0200
@@ -100,8 +100,8 @@
{splits = splits, inj_consts = update (op =) c inj_consts,
discrete = discrete});
-val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9;
-val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9;
+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);
structure LA_Data =
--- a/src/HOL/Tools/meson.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/HOL/Tools/meson.ML Sun Mar 28 16:59:06 2010 +0200
@@ -48,7 +48,7 @@
fun trace_msg msg = if ! trace then tracing (msg ()) else ();
val max_clauses_default = 60;
-val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
+val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default);
val disj_forward = @{thm disj_forward};
val disj_forward2 = @{thm disj_forward2};
--- a/src/Provers/blast.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/Provers/blast.ML Sun Mar 28 16:59:06 2010 +0200
@@ -1275,7 +1275,7 @@
(*Public version with fixed depth*)
fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
-val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20;
+val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
fun blast_tac cs i st =
((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
--- a/src/Pure/meta_simplifier.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/Pure/meta_simplifier.ML Sun Mar 28 16:59:06 2010 +0200
@@ -251,7 +251,7 @@
(* simp depth *)
-val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
+val simp_depth_limit_value = Config.declare false "simp_depth_limit" (K (Config.Int 100));
val simp_depth_limit = Config.int simp_depth_limit_value;
val trace_simp_depth_limit = Unsynchronized.ref 1;
@@ -274,10 +274,10 @@
exception SIMPLIFIER of string * thm;
-val debug_simp_value = Config.declare false "debug_simp" (Config.Bool false);
+val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
val debug_simp = Config.bool debug_simp_value;
-val trace_simp_value = Config.declare false "trace_simp" (Config.Bool false);
+val trace_simp_value = Config.declare false "trace_simp" (K (Config.Bool false));
val trace_simp = Config.bool trace_simp_value;
val trace_simp_ref = Unsynchronized.ref false;
--- a/src/Pure/unify.ML Sun Mar 28 16:13:29 2010 +0200
+++ b/src/Pure/unify.ML Sun Mar 28 16:59:06 2010 +0200
@@ -32,19 +32,19 @@
(*Unification options*)
(*tracing starts above this depth, 0 for full*)
-val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 50);
+val trace_bound_value = Config.declare true "unify_trace_bound" (K (Config.Int 50));
val trace_bound = Config.int trace_bound_value;
(*unification quits above this depth*)
-val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 60);
+val search_bound_value = Config.declare true "unify_search_bound" (K (Config.Int 60));
val search_bound = Config.int search_bound_value;
(*print dpairs before calling SIMPL*)
-val trace_simp_value = Config.declare true "unify_trace_simp" (Config.Bool false);
+val trace_simp_value = Config.declare true "unify_trace_simp" (K (Config.Bool false));
val trace_simp = Config.bool trace_simp_value;
(*announce potential incompleteness of type unification*)
-val trace_types_value = Config.declare true "unify_trace_types" (Config.Bool false);
+val trace_types_value = Config.declare true "unify_trace_types" (K (Config.Bool false));
val trace_types = Config.bool trace_types_value;