# HG changeset patch
# User wenzelm
# Date 1269788346 -7200
# Node ID 992839c4be90c92fece31063d6a13b634381884d
# Parent  5560b2437789429386a9c95ceab3ef601470dec0
static defaults for configuration options;

diff -r 5560b2437789 -r 992839c4be90 src/HOL/Mirabelle/Tools/mirabelle.ML
--- 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
 
diff -r 5560b2437789 -r 992839c4be90 src/HOL/SMT/Tools/smt_normalize.ML
--- 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}]
diff -r 5560b2437789 -r 992839c4be90 src/HOL/SMT/Tools/smt_solver.ML
--- 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
 (
diff -r 5560b2437789 -r 992839c4be90 src/HOL/SMT/Tools/z3_proof_rules.ML
--- 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}
diff -r 5560b2437789 -r 992839c4be90 src/HOL/SMT/Tools/z3_solver.ML
--- 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
 
diff -r 5560b2437789 -r 992839c4be90 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- 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 *)
diff -r 5560b2437789 -r 992839c4be90 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- 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 *)
 
diff -r 5560b2437789 -r 992839c4be90 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- 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;
 
diff -r 5560b2437789 -r 992839c4be90 src/HOL/Tools/inductive_codegen.ML
--- 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
diff -r 5560b2437789 -r 992839c4be90 src/HOL/Tools/lin_arith.ML
--- 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 =
diff -r 5560b2437789 -r 992839c4be90 src/HOL/Tools/meson.ML
--- 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};
diff -r 5560b2437789 -r 992839c4be90 src/Provers/blast.ML
--- 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)
diff -r 5560b2437789 -r 992839c4be90 src/Pure/meta_simplifier.ML
--- 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;
 
diff -r 5560b2437789 -r 992839c4be90 src/Pure/unify.ML
--- 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;