# HG changeset patch
# User wenzelm
# Date 1614960152 -3600
# Node ID 3fb201ca8fb5a051d398a5a2af73d43cf795693d
# Parent  1892708fd14864665202793339297aa2dd26c7da
tuned --- more elementary Time operations;

diff -r 1892708fd148 -r 3fb201ca8fb5 src/HOL/Tools/Nitpick/nitpick.ML
--- 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
 
diff -r 1892708fd148 -r 3fb201ca8fb5 src/HOL/Tools/Nunchaku/nunchaku.ML
--- 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
diff -r 1892708fd148 -r 3fb201ca8fb5 src/HOL/Tools/try0.ML
--- 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;