# HG changeset patch
# User blanchet
# Date 1307542818 -7200
# Node ID 07eb0ad9bb93550e51ea0c0b6e98b437f439d4bd
# Parent  0f2bbcfaf208dbcb1c7c7d283a73e2583080c9a5
renamed option to avoid talking about seconds, since this is now the default Isabelle unit

diff -r 0f2bbcfaf208 -r 07eb0ad9bb93 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 16:20:18 2011 +0200
@@ -19,7 +19,7 @@
   val timeoutN : string
   val unknownN : string
   val auto_minimize_min_facts : int Config.T
-  val auto_minimize_max_seconds : real Config.T
+  val auto_minimize_max_time : real Config.T
   val get_minimizing_prover : Proof.context -> mode -> string -> prover
   val run_sledgehammer :
     params -> mode -> int -> relevance_override -> (string -> minimize_command)
@@ -69,8 +69,8 @@
 val auto_minimize_min_facts =
   Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
       (fn generic => Config.get_generic generic binary_min_facts)
-val auto_minimize_max_seconds =
-  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
+val auto_minimize_max_time =
+  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
       (K 5.0)
 
 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
@@ -90,7 +90,7 @@
             let
               fun can_min_fast_enough msecs =
                 0.001 * Real.fromInt ((num_facts + 2) * msecs)
-                <= Config.get ctxt auto_minimize_max_seconds
+                <= Config.get ctxt auto_minimize_max_time
               val prover_fast_enough =
                 run_time_in_msecs |> Option.map can_min_fast_enough
                                   |> the_default false