src/Pure/Concurrent/task_queue.ML

--- a/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -139,7 +139,7 @@
     let
       val start = Time.now ();
       val result = Exn.capture (restore_attributes e) ();
-      val t = Time.- (Time.now (), start);
+      val t = Time.now () - start;
       val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
     in Exn.release result end) ();
 
@@ -167,14 +167,14 @@
 (* timing *)
 
 fun running task =
-  update_timing (fn t => fn (a, b, ds) => (Time.+ (a, t), b, ds)) task;
+  update_timing (fn t => fn (a, b, ds) => (a + t, b, ds)) task;
 
 fun joining task =
-  update_timing (fn t => fn (a, b, ds) => (Time.- (a, t), b, ds)) task;
+  update_timing (fn t => fn (a, b, ds) => (a - t, b, ds)) task;
 
 fun waiting task deps =
   update_timing (fn t => fn (a, b, ds) =>
-    (Time.- (a, t), Time.+ (b, t),
+    (a - t, b + t,
       if ! Multithreading.trace > 0
       then fold (insert (op =) o name_of_task) deps ds else ds)) task;