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,
+     run_time: Time.time,
      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,
+   run_time: Time.time,
    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 = msecs,
+    {outcome = outcome, used_facts = used_facts, run_time = Time.fromMilliseconds 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

             facts |> take new_num_facts
                   |> 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 = Time.toMilliseconds time_so_far}
+           used_facts = used_facts, run_time = 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

   let
     val ctxt = Proof.context_of state
     val num_facts = length facts
     val facts = facts ~~ (0 upto num_facts - 1)
                 |> map (smt_weighted_fact ctxt num_facts)
-    val {outcome, used_facts, run_time_in_msecs} =
+    val {outcome, used_facts, run_time} =
       smt_filter_loop ctxt name params state subgoal smt_filter facts
     val (used_facts, used_ths) = used_facts |> ListPair.unzip
     val outcome = outcome |> Option.map failure_from_smt_failure
     val (preplay, message, message_tail) =
       case outcome of

                 (preplay, proof_banner mode name, used_facts,
                  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 run_time_in_msecs) ^ "."
+           "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
          else
            "")
       | SOME failure =>
         (K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   in
-    {outcome = outcome, used_facts = used_facts,
-     run_time_in_msecs = run_time_in_msecs, preplay = preplay,
-     message = message, message_tail = message_tail}
+    {outcome = outcome, used_facts = used_facts, run_time = run_time,
+     preplay = preplay, message = message, message_tail = message_tail}
   end
 
 fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
               ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let

       facts |> map untranslated_fact |> ListPair.unzip
   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 = Time.toMilliseconds time,
+      {outcome = NONE, used_facts = used_facts, run_time = 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 = ~1,
+        {outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
          preplay = K play, message = fn _ => string_for_failure failure,
          message_tail = ""}
       end
   end