1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Sep 12 09:07:23 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Sep 12 10:49:37 2011 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4    val noneN : string
     1.5    val timeoutN : string
     1.6    val unknownN : string
     1.7 -  val auto_min_min_facts : int Config.T
     1.8 -  val auto_min_max_time : real Config.T
     1.9 +  val auto_minimize_min_facts : int Config.T
    1.10 +  val auto_minimize_max_time : real Config.T
    1.11    val get_minimizing_prover : Proof.context -> mode -> string -> prover
    1.12    val run_sledgehammer :
    1.13      params -> mode -> int -> relevance_override -> (string -> minimize_command)
    1.14 @@ -66,11 +66,12 @@
    1.15      else
    1.16        "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
    1.17  
    1.18 -val auto_min_min_facts =
    1.19 -  Attrib.setup_config_int @{binding sledgehammer_auto_min_min_facts}
    1.20 +val auto_minimize_min_facts =
    1.21 +  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
    1.22        (fn generic => Config.get_generic generic binary_min_facts)
    1.23 -val auto_min_max_time =
    1.24 -  Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 5.0)
    1.25 +val auto_minimize_max_time =
    1.26 +  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
    1.27 +                           (K 5.0)
    1.28  
    1.29  fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    1.30               ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    1.31 @@ -83,13 +84,13 @@
    1.32        val num_facts = length used_facts
    1.33        val ((minimize, minimize_name), preplay) =
    1.34          if mode = Normal then
    1.35 -          if num_facts >= Config.get ctxt auto_min_min_facts then
    1.36 +          if num_facts >= Config.get ctxt auto_minimize_min_facts then
    1.37              ((true, name), preplay)
    1.38            else
    1.39              let
    1.40                fun can_min_fast_enough msecs =
    1.41                  0.001 * Real.fromInt ((num_facts + 2) * msecs)
    1.42 -                <= Config.get ctxt auto_min_max_time
    1.43 +                <= Config.get ctxt auto_minimize_max_time
    1.44                val prover_fast_enough =
    1.45                  run_time_in_msecs |> Option.map can_min_fast_enough
    1.46                                    |> the_default false