src/Pure/General/timing.ML
changeset 67001 b34fbf33a7ea
parent 67000 1698e9ccef2d
child 67932 04352338f7f3
     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;