1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Oct 09 16:40:03 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Oct 09 17:21:28 2013 +0200
     1.3 @@ -88,8 +88,7 @@
     1.4    val problem_prefix : string Config.T
     1.5    val completish : bool Config.T
     1.6    val atp_full_names : bool Config.T
     1.7 -  val smt_builtin_facts : bool Config.T
     1.8 -  val smt_builtin_trans : bool Config.T
     1.9 +  val smt_builtins : bool Config.T
    1.10    val smt_triggers : bool Config.T
    1.11    val smt_weights : bool Config.T
    1.12    val smt_weight_min_facts : int Config.T
    1.13 @@ -158,27 +157,18 @@
    1.14  (** The Sledgehammer **)
    1.15  
    1.16  (* Empty string means create files in Isabelle's temporary files directory. *)
    1.17 -val dest_dir =
    1.18 -  Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
    1.19 -val problem_prefix =
    1.20 -  Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
    1.21 -val completish =
    1.22 -  Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
    1.23 +val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
    1.24 +val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
    1.25 +val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
    1.26  
    1.27  (* In addition to being easier to read, readable names are often much shorter,
    1.28     especially if types are mangled in names. This makes a difference for some
    1.29     provers (e.g., E). For these reason, short names are enabled by default. *)
    1.30 -val atp_full_names =
    1.31 -  Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
    1.32 +val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
    1.33  
    1.34 -val smt_builtin_facts =
    1.35 -  Attrib.setup_config_bool @{binding sledgehammer_smt_builtin_facts} (K true)
    1.36 -val smt_builtin_trans =
    1.37 -  Attrib.setup_config_bool @{binding sledgehammer_smt_builtin_trans} (K true)
    1.38 -val smt_triggers =
    1.39 -  Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    1.40 -val smt_weights =
    1.41 -  Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
    1.42 +val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
    1.43 +val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    1.44 +val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
    1.45  val smt_weight_min_facts =
    1.46    Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
    1.47  
    1.48 @@ -1023,7 +1013,7 @@
    1.49                   I)
    1.50             |> Config.put SMT_Config.infer_triggers
    1.51                           (Config.get ctxt smt_triggers)
    1.52 -           |> not (Config.get ctxt smt_builtin_trans)
    1.53 +           |> not (Config.get ctxt smt_builtins)
    1.54                ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
    1.55                   #> Config.put SMT_Config.datatypes false)
    1.56             |> repair_monomorph_context max_mono_iters default_max_mono_iters