tuned;
authorwenzelm
Sat Nov 04 12:39:25 2017 +0100 (7 months ago)
changeset 67001b34fbf33a7ea
parent 67000 1698e9ccef2d
child 67002 e8d64340d58b
tuned;
src/Pure/General/timing.ML
     1.1 --- a/src/Pure/General/timing.ML	Sat Nov 04 12:25:09 2017 +0100
     1.2 +++ b/src/Pure/General/timing.ML	Sat Nov 04 12:39:25 2017 +0100
     1.3 @@ -57,7 +57,6 @@
     1.4      val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
     1.5        Timer.checkCPUTimes cpu_timer;
     1.6  
     1.7 -    open Time;
     1.8      val elapsed = real_time2 - real_time;
     1.9      val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    1.10      val cpu = usr2 - usr + sys2 - sys + gc;