changeset 67001 | b34fbf33a7ea |
parent 67000 | 1698e9ccef2d |
child 67932 | 04352338f7f3 |
--- a/src/Pure/General/timing.ML Sat Nov 04 12:25:09 2017 +0100 +++ b/src/Pure/General/timing.ML Sat Nov 04 12:39:25 2017 +0100 @@ -57,7 +57,6 @@ val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} = Timer.checkCPUTimes cpu_timer; - open Time; val elapsed = real_time2 - real_time; val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; val cpu = usr2 - usr + sys2 - sys + gc;