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