--- 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