1.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon May 02 13:29:47 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon May 02 16:33:21 2011 +0200
     1.3 @@ -23,12 +23,10 @@
     1.4    (*options*)
     1.5    val oracle: bool Config.T
     1.6    val datatypes: bool Config.T
     1.7 -  val timeoutN: string
     1.8    val timeout: real Config.T
     1.9    val random_seed: int Config.T
    1.10    val fixed: bool Config.T
    1.11    val verbose: bool Config.T
    1.12 -  val traceN: string
    1.13    val trace: bool Config.T
    1.14    val trace_used_facts: bool Config.T
    1.15    val monomorph_limit: int Config.T
    1.16 @@ -149,75 +147,21 @@
    1.17  
    1.18  (* options *)
    1.19  
    1.20 -val oracleN = "smt_oracle"
    1.21 -val (oracle, setup_oracle) = Attrib.config_bool oracleN (K true)
    1.22 -
    1.23 -val datatypesN = "smt_datatypes"
    1.24 -val (datatypes, setup_datatypes) = Attrib.config_bool datatypesN (K false)
    1.25 -
    1.26 -val timeoutN = "smt_timeout"
    1.27 -val (timeout, setup_timeout) = Attrib.config_real timeoutN (K 30.0)
    1.28 -
    1.29 -val random_seedN = "smt_random_seed"
    1.30 -val (random_seed, setup_random_seed) = Attrib.config_int random_seedN (K 1)
    1.31 -
    1.32 -val fixedN = "smt_fixed"
    1.33 -val (fixed, setup_fixed) = Attrib.config_bool fixedN (K false)
    1.34 -
    1.35 -val verboseN = "smt_verbose"
    1.36 -val (verbose, setup_verbose) = Attrib.config_bool verboseN (K true)
    1.37 -
    1.38 -val traceN = "smt_trace"
    1.39 -val (trace, setup_trace) = Attrib.config_bool traceN (K false)
    1.40 -
    1.41 -val trace_used_factsN = "smt_trace_used_facts"
    1.42 -val (trace_used_facts, setup_trace_used_facts) =
    1.43 -  Attrib.config_bool trace_used_factsN (K false)
    1.44 -
    1.45 -val monomorph_limitN = "smt_monomorph_limit"
    1.46 -val (monomorph_limit, setup_monomorph_limit) =
    1.47 -  Attrib.config_int monomorph_limitN (K 10)
    1.48 -
    1.49 -val monomorph_instancesN = "smt_monomorph_instances"
    1.50 -val (monomorph_instances, setup_monomorph_instances) =
    1.51 -  Attrib.config_int monomorph_instancesN (K 500)
    1.52 -
    1.53 -val monomorph_fullN = "smt_monomorph_full"
    1.54 -val (monomorph_full, setup_monomorph_full) =
    1.55 -  Attrib.config_bool monomorph_fullN (K true)
    1.56 -
    1.57 -val infer_triggersN = "smt_infer_triggers"
    1.58 -val (infer_triggers, setup_infer_triggers) =
    1.59 -  Attrib.config_bool infer_triggersN (K false)
    1.60 -
    1.61 -val drop_bad_factsN = "smt_drop_bad_facts"
    1.62 -val (drop_bad_facts, setup_drop_bad_facts) =
    1.63 -  Attrib.config_bool drop_bad_factsN (K false)
    1.64 -
    1.65 -val filter_only_factsN = "smt_filter_only_facts"
    1.66 -val (filter_only_facts, setup_filter_only_facts) =
    1.67 -  Attrib.config_bool filter_only_factsN (K false)
    1.68 -
    1.69 -val debug_filesN = "smt_debug_files"
    1.70 -val (debug_files, setup_debug_files) =
    1.71 -  Attrib.config_string debug_filesN (K "")
    1.72 -
    1.73 -val setup_options =
    1.74 -  setup_oracle #>
    1.75 -  setup_datatypes #>
    1.76 -  setup_timeout #>
    1.77 -  setup_random_seed #>
    1.78 -  setup_fixed #>
    1.79 -  setup_trace #>
    1.80 -  setup_verbose #>
    1.81 -  setup_monomorph_limit #>
    1.82 -  setup_monomorph_instances #>
    1.83 -  setup_monomorph_full #>
    1.84 -  setup_infer_triggers #>
    1.85 -  setup_drop_bad_facts #>
    1.86 -  setup_filter_only_facts #>
    1.87 -  setup_trace_used_facts #>
    1.88 -  setup_debug_files
    1.89 +val oracle = Attrib.setup_config_bool @{binding smt_oracle} (K true)
    1.90 +val datatypes = Attrib.setup_config_bool @{binding smt_datatypes} (K false)
    1.91 +val timeout = Attrib.setup_config_real @{binding smt_timeout} (K 30.0)
    1.92 +val random_seed = Attrib.setup_config_int @{binding smt_random_seed} (K 1)
    1.93 +val fixed = Attrib.setup_config_bool @{binding smt_fixed} (K false)
    1.94 +val verbose = Attrib.setup_config_bool @{binding smt_verbose} (K true)
    1.95 +val trace = Attrib.setup_config_bool @{binding smt_trace} (K false)
    1.96 +val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
    1.97 +val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
    1.98 +val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
    1.99 +val monomorph_full = Attrib.setup_config_bool @{binding smt_monomorph_full} (K true)
   1.100 +val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
   1.101 +val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
   1.102 +val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
   1.103 +val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
   1.104  
   1.105  
   1.106  (* diagnostics *)
   1.107 @@ -269,7 +213,6 @@
   1.108  
   1.109  val setup =
   1.110    setup_solver #>
   1.111 -  setup_options #>
   1.112    setup_certificates
   1.113  
   1.114  fun print_setup ctxt =