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