src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

      smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
 
   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}
 
   type prover =

    smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
 
 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}
 
 type prover =

               ""))
         end
       | 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
 
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
    these are sorted out properly in the SMT module, we have to interpret these

                   |> do_slice timeout (slice + 1) outcome0 time_so_far
           end
         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
 
 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
         minimize_command

                  choose_minimize_command minimize_command name preplay,
                  subgoal, subgoal_count)
             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 =>
         (K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   in

   in
     case play_one_line_proof debug timeout used_ths state subgoal
                              [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
                       val one_line_params =
                          (play, proof_banner mode name, used_facts,

        message_tail = ""}
     | play =>
       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
   end