make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 04 15:31:26 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 05 09:05:22 2010 +0100
@@ -369,10 +369,11 @@
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
-    val ({outcome, message, used_facts, run_time_in_msecs = SOME time_prover, ...}
+    val ({outcome, message, used_facts, run_time_in_msecs, ...}
          : Sledgehammer.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time
                       (prover params (K ""))) problem
+    val time_prover = run_time_in_msecs |> the_default ~1
   in
     case outcome of
       NONE => (message, SH_OK (time_isa, time_prover, used_facts))