minimize automatically even if Metis failed, if the external prover was really fast

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon May 30 17:00:38 2011 +0200
@@ -160,7 +160,7 @@
     val ctxt = Proof.context_of state
     val prover = get_prover ctxt Minimize prover_name
     val msecs = Time.toMilliseconds timeout
-    val _ = print silent (fn () => "Sledgehammer minimize: " ^
+    val _ = print silent (fn () => "Sledgehammer minimizer: " ^
                                    quote prover_name ^ ".")
     fun do_test timeout =
       test_facts params explicit_apply_opt silent prover timeout i n state

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 30 17:00:38 2011 +0200
@@ -19,6 +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 get_minimizing_prover : Proof.context -> mode -> string -> prover
   val run_sledgehammer :
     params -> mode -> int -> relevance_override -> (string -> minimize_command)
@@ -67,7 +68,6 @@
 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}
       (K 5.0)
@@ -82,6 +82,9 @@
          else
            let
              val num_facts = length used_facts
+             fun can_minimize_fast_enough msecs =
+               0.001 * Real.fromInt ((num_facts + 2) * msecs)
+               <= Config.get ctxt auto_minimize_max_seconds
              val ((minimize, minimize_name), preplay) =
                if mode = Normal then
                  if num_facts >= Config.get ctxt auto_minimize_min_facts then
@@ -90,11 +93,13 @@
                    let val preplay = preplay () in
                      (case preplay of
                         Played (reconstructor, timeout) =>
-                        (0.001 * Real.fromInt ((num_facts + 2)
-                                               * Time.toMilliseconds timeout)
-                        <= Config.get ctxt auto_minimize_max_seconds,
-                        reconstructor_name reconstructor)
-                      | _ => (false, name), K preplay)
+                        (can_minimize_fast_enough (Time.toMilliseconds timeout),
+                         reconstructor_name reconstructor)
+                      | _ =>
+                        case run_time_in_msecs of
+                          SOME msecs => (can_minimize_fast_enough msecs, name)
+                        | NONE => (false, name),
+                     K preplay)
                    end
                else
                  ((false, name), preplay)
@@ -196,9 +201,10 @@
       let
         val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
       in
-        (if outcome_code = someN then message ()
-         else if mode = Normal then quote name ^ ": " ^ message ()
-         else "")
+        (if outcome_code = someN orelse mode = Normal then
+           quote name ^ ": " ^ message ()
+         else
+           "")
         |> Async_Manager.break_into_chunks
         |> List.app Output.urgent_message;
         (outcome_code, state)