src/Pure/Tools/build.ML
changeset 62826 eb94e570c1a4
parent 62793 f235646b1b73
child 62884 66494de0aafe
     1.1 --- a/src/Pure/Tools/build.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    (case Markup.parse_command_timing_properties props of
     1.5      SOME ({file, offset, name}, time) =>
     1.6        Symtab.map_default (file, Inttab.empty)
     1.7 -        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
     1.8 +        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
     1.9    | NONE => I);
    1.10  
    1.11  fun approximative_id name pos =
    1.12 @@ -83,7 +83,7 @@
    1.13            val {elapsed, ...} = Markup.parse_timing_properties args;
    1.14            val is_significant =
    1.15              Timing.is_relevant_time elapsed andalso
    1.16 -            Time.>= (elapsed, Options.default_seconds "command_timing_threshold");
    1.17 +            elapsed >= Options.default_seconds "command_timing_threshold";
    1.18          in
    1.19            if is_significant then
    1.20              (case approximative_id name pos of