src/Pure/General/timing.ML
changeset 82092 93195437fdee
parent 82086 e0edf30885ef
--- a/src/Pure/General/timing.ML	Thu Feb 06 12:18:56 2025 +0100
+++ b/src/Pure/General/timing.ML	Thu Feb 06 12:46:13 2025 +0100
@@ -86,9 +86,9 @@
   is_relevant_time gc;
 
 fun message {elapsed, cpu, gc} =
-  Value.print_time elapsed ^ "s elapsed time, " ^
-  Value.print_time cpu ^ "s cpu time, " ^
-  Value.print_time gc ^ "s GC time" handle Time.Time => "";
+  Time.message elapsed ^ " elapsed time, " ^
+  Time.message cpu ^ " cpu time, " ^
+  Time.message gc ^ " GC time" handle Time.Time => "";
 
 fun cond_timeit enabled msg e =
   if enabled then