diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Tools/build.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -22,7 +22,7 @@
   (case Markup.parse_command_timing_properties props of
     SOME ({file, offset, name}, time) =>
       Symtab.map_default (file, Inttab.empty)
-        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
+        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
   | NONE => I);
 
 fun approximative_id name pos =
@@ -83,7 +83,7 @@
           val {elapsed, ...} = Markup.parse_timing_properties args;
           val is_significant =
             Timing.is_relevant_time elapsed andalso
-            Time.>= (elapsed, Options.default_seconds "command_timing_threshold");
+            elapsed >= Options.default_seconds "command_timing_threshold";
         in
           if is_significant then
             (case approximative_id name pos of