src/Pure/General/timing.ML
changeset 67000 1698e9ccef2d
parent 66415 96ad7d5ff613
child 67001 b34fbf33a7ea
--- a/src/Pure/General/timing.ML	Sat Nov 04 11:42:08 2017 +0100
+++ b/src/Pure/General/timing.ML	Sat Nov 04 12:25:09 2017 +0100
@@ -84,9 +84,9 @@
   is_relevant_time gc;
 
 fun message {elapsed, cpu, gc} =
-  Time.toString elapsed ^ "s elapsed time, " ^
-  Time.toString cpu ^ "s cpu time, " ^
-  Time.toString gc ^ "s GC time" handle Time.Time => "";
+  Value.print_time elapsed ^ "s elapsed time, " ^
+  Value.print_time cpu ^ "s cpu time, " ^
+  Value.print_time gc ^ "s GC time" handle Time.Time => "";
 
 fun cond_timeit enabled msg e =
   if enabled then