--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 05 16:45:16 2021 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 05 17:02:32 2021 +0100
@@ -201,7 +201,6 @@
subst def_assm_ts nondef_assm_ts orig_t =
let
val time_start = Time.now ()
- val timer = Timer.startRealTimer ()
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val keywords = Thy_Header.get_keywords thy
@@ -933,8 +932,7 @@
handle Timeout.TIMEOUT _ =>
(print_nt (fn () => excipit "ran out of time after checking");
if !met_potential > 0 then potentialN else unknownN)
- val _ = print_v (fn () =>
- "Total time: " ^ string_of_time (Timer.checkRealTimer timer))
+ val _ = print_v (fn () => "Total time: " ^ string_of_time (Time.now () - time_start))
val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code))
in (outcome_code, Queue.content (Synchronized.value outcome)) end
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML Fri Mar 05 16:45:16 2021 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML Fri Mar 05 17:02:32 2021 +0100
@@ -159,7 +159,7 @@
let
val ctxt = Proof.context_of state;
- val timer = Timer.startRealTimer ()
+ val time_start = Time.now ()
val print = writeln;
val print_n = if mode = Normal then writeln else K ();
@@ -310,10 +310,10 @@
val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode"));
val outcome as (outcome_code, _) =
- Timeout.apply (Time.+ (timeout, timeout_slack)) run ()
+ Timeout.apply (timeout + timeout_slack) run ()
handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE));
- val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer));
+ val _ = print_v (fn () => "Total time: " ^ string_of_time (Time.now () - time_start));
val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code));
in
--- a/src/HOL/Tools/try0.ML Fri Mar 05 16:45:16 2021 +0100
+++ b/src/HOL/Tools/try0.ML Fri Mar 05 17:02:32 2021 +0100
@@ -34,9 +34,9 @@
end;
fun apply_generic timeout_opt name command pre post apply st =
- let val timer = Timer.startRealTimer () in
+ let val time_start = Time.now () in
if try (can_apply timeout_opt pre post apply) st = SOME true then
- SOME (name, command, Time.toMilliseconds (Timer.checkRealTimer timer))
+ SOME (name, command, Time.toMilliseconds (Time.now () - time_start))
else
NONE
end;