# HG changeset patch
# User blanchet
# Date 1320583586 -3600
# Node ID fbf2e1bdbf16620f8dea15419728dc416915ec1c
# Parent  ff2edf24e83a344b43dde68e99f86a78d15dd5bb
tune: no need for option

diff -r ff2edf24e83a -r fbf2e1bdbf16 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 13:37:49 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Nov 06 13:46:26 2011 +0100
@@ -80,11 +80,9 @@
               | NONE =>
                 "Found proof" ^
                  (if length used_facts = length facts then ""
-                  else " with " ^ n_facts used_facts) ^
-                 (case run_time_in_msecs of
-                    SOME ms =>
-                    " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
-                  | NONE => "") ^ ".");
+                  else " with " ^ n_facts used_facts) ^ " (" ^
+                 string_from_time (Time.fromMilliseconds run_time_in_msecs) ^
+                 ").");
     result
   end
 
diff -r ff2edf24e83a -r fbf2e1bdbf16 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Nov 06 13:37:49 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Nov 06 13:46:26 2011 +0100
@@ -52,7 +52,7 @@
   type prover_result =
     {outcome: failure option,
      used_facts: (string * locality) list,
-     run_time_in_msecs: int option,
+     run_time_in_msecs: int,
      preplay: unit -> play,
      message: play -> string,
      message_tail: string}
@@ -323,7 +323,7 @@
 type prover_result =
   {outcome: failure option,
    used_facts: (string * locality) list,
-   run_time_in_msecs: int option,
+   run_time_in_msecs: int,
    preplay: unit -> play,
    message: play -> string,
    message_tail: string}
@@ -797,7 +797,7 @@
       | SOME failure =>
         ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   in
-    {outcome = outcome, used_facts = used_facts, run_time_in_msecs = SOME msecs,
+    {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
      preplay = preplay, message = message, message_tail = message_tail}
   end
 
@@ -929,7 +929,7 @@
         else
           {outcome = if is_none outcome then NONE else the outcome0,
            used_facts = used_facts,
-           run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}
+           run_time_in_msecs = Time.toMilliseconds time_so_far}
       end
   in do_slice timeout 1 NONE Time.zeroTime end
 
@@ -969,8 +969,7 @@
             in one_line_proof_text one_line_params end,
          if verbose then
            "\nSMT solver real CPU time: " ^
-           string_from_time (Time.fromMilliseconds
-                                 (the run_time_in_msecs)) ^ "."
+           string_from_time (Time.fromMilliseconds run_time_in_msecs) ^ "."
          else
            "")
       | SOME failure =>
@@ -995,7 +994,7 @@
                              [reconstructor] of
       play as Played (_, time) =>
       {outcome = NONE, used_facts = used_facts,
-       run_time_in_msecs = SOME (Time.toMilliseconds time),
+       run_time_in_msecs = Time.toMilliseconds time,
        preplay = K play,
        message = fn play =>
                     let
@@ -1008,7 +1007,7 @@
       let
         val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
       in
-        {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
+        {outcome = SOME failure, used_facts = [], run_time_in_msecs = ~1,
          preplay = K play, message = fn _ => string_for_failure failure,
          message_tail = ""}
       end
diff -r ff2edf24e83a -r fbf2e1bdbf16 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun Nov 06 13:37:49 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun Nov 06 13:46:26 2011 +0100
@@ -91,9 +91,7 @@
               fun can_min_fast_enough msecs =
                 0.001 * Real.fromInt ((num_facts + 2) * msecs)
                 <= Config.get ctxt auto_minimize_max_time
-              val prover_fast_enough =
-                run_time_in_msecs |> Option.map can_min_fast_enough
-                                  |> the_default false
+              val prover_fast_enough = can_min_fast_enough run_time_in_msecs
             in
               if isar_proof then
                 ((prover_fast_enough, name), preplay)