# HG changeset patch
# User blanchet
# Date 1288944322 -3600
# Node ID 443b426e05ea6d98bfa27666ebedacc35fe61e40
# Parent  ff0e17a9d84058cb0cf39794432ba0c2af02e961
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information

diff -r ff0e17a9d840 -r 443b426e05ea src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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))