# HG changeset patch
# User wenzelm
# Date 1459632545 -7200
# Node ID eb94e570c1a45d43a2d691631d70b4137c918f5f
# Parent  e6e80a8bf624bc120648c40b1321e17e76a69afe
prefer infix operations;

diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -541,7 +541,7 @@
         val facts = named_thms |> map (ref_of_str o fst o fst)
         val fact_override = {add = facts, del = [], only = true}
         fun my_timeout time_slice =
-          timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
+          timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal
         fun sledge_tac time_slice prover type_enc =
           Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
             (override_params prover type_enc (my_timeout time_slice)) fact_override []
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -989,7 +989,7 @@
 val fudge_ms = 250
 
 fun milliseconds_until_deadline deadline =
-  Int.max (0, Time.toMilliseconds (Time.- (deadline, Time.now ())) - fudge_ms)
+  Int.max (0, Time.toMilliseconds (deadline - Time.now ()) - fudge_ms)
 
 fun uncached_solve_any_problem overlord deadline max_threads max_solutions
                                problems =
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -251,7 +251,7 @@
     fun check_deadline () =
       let val t = Time.now () in
         if Time.compare (t, deadline) <> LESS
-        then raise Timeout.TIMEOUT (Time.- (t, time_start))
+        then raise Timeout.TIMEOUT (t - time_start)
         else ()
       end
 
@@ -540,7 +540,7 @@
         val bit_width = if bits = 0 then 16 else bits + 1
         val delay =
           if unsound then
-            unsound_delay_for_timeout (Time.- (deadline, Time.now ()))
+            unsound_delay_for_timeout (deadline - Time.now ())
           else
             0
         val settings = [("solver", commas_quote kodkod_sat_solver),
@@ -986,9 +986,9 @@
     else
       let
         val unknown_outcome = (unknownN, [])
-        val deadline = Time.+ (Time.now (), timeout)
+        val deadline = Time.now () + timeout
         val outcome as (outcome_code, _) =
-          Timeout.apply (Time.+ (timeout, timeout_bonus))
+          Timeout.apply (timeout + timeout_bonus)
               (pick_them_nits_in_term deadline state params mode i n step subst
                                       def_assm_ts nondef_assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -96,7 +96,7 @@
       let
         fun time_limit timeout_heap =
           (case try Thread_Heap.min timeout_heap of
-            NONE => Time.+ (Time.now (), max_wait_time)
+            NONE => Time.now () + max_wait_time
           | SOME (time, _) => time)
 
         (*action: find threads whose timeout is reached, and interrupt canceling threads*)
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -460,7 +460,7 @@
 fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
   (case play of
     Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
-  | Play_Timed_Out time => Time.> (time, Time.zeroTime)
+  | Play_Timed_Out time => time > Time.zeroTime
   | Play_Failed => true)
 
 fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -103,8 +103,8 @@
 val merge_slack_factor = 1.5
 
 fun adjust_merge_timeout max time =
-  let val timeout = time_mult merge_slack_factor (Time.+ (merge_slack_time, time)) in
-    if Time.< (max, timeout) then max else timeout
+  let val timeout = time_mult merge_slack_factor (merge_slack_time + time) in
+    if max < timeout then max else timeout
   end
 
 val compress_degree = 2
@@ -171,7 +171,7 @@
               val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment)
 
               (* check if the modified step can be preplayed fast enough *)
-              val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
+              val timeout = adjust_merge_timeout preplay_timeout (time + reference_time l')
             in
               (case preplay_isar_step ctxt [] timeout hopeless step'' of
                 meths_outcomes as (_, Played time'') :: _ =>
@@ -215,7 +215,7 @@
               | SOME times0 =>
                 let
                   val n = length labels
-                  val total_time = Library.foldl Time.+ (reference_time l, times0)
+                  val total_time = Library.foldl (op +) (reference_time l, times0)
                   val timeout = adjust_merge_timeout preplay_timeout
                     (Time.fromReal (Time.toReal total_time / Real.fromInt n))
                   val meths_outcomess =
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -45,7 +45,7 @@
 
     fun minimize_half _ min_facts [] time = (min_facts, time)
       | minimize_half mk_step min_facts (fact :: facts) time =
-        (case preplay_isar_step_for_method ctxt [] (Time.+ (time, slack)) meth
+        (case preplay_isar_step_for_method ctxt [] (time + slack) meth
             (mk_step (min_facts @ facts)) of
           Played time' => minimize_half mk_step min_facts facts time'
         | _ => minimize_half mk_step (fact :: min_facts) facts time)
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -52,7 +52,7 @@
 
       fun apply_f x =
         let val timeout = !next_timeout in
-          if Time.<= (timeout, min_timeout) then
+          if timeout <= min_timeout then
             NONE
           else
             let val y = f timeout x in
@@ -188,7 +188,7 @@
 
 fun add_preplay_outcomes Play_Failed _ = Play_Failed
   | add_preplay_outcomes _ Play_Failed = Play_Failed
-  | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
+  | add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2)
   | add_preplay_outcomes play1 play2 =
     Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2)))
 
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -168,7 +168,7 @@
 
 fun normalize_scores _ [] = []
   | normalize_scores max_facts xs =
-    map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
+    map (apsnd (curry (op *) (1.0 / avg (map snd (take max_facts xs))))) xs
 
 fun mesh_facts maybe_distinct _ max_facts [(_, (sels, unks))] =
     map fst (take max_facts sels) @ take (max_facts - length sels) unks
@@ -655,7 +655,7 @@
     (case try OS.FileSys.modTime (File.platform_path path) of
       NONE => time_state
     | SOME disk_time =>
-      if Time.>= (memory_time, disk_time) then
+      if memory_time >= disk_time then
         time_state
       else
         (disk_time,
@@ -700,7 +700,7 @@
       val dirty_facts' =
         (case try OS.FileSys.modTime (File.platform_path path) of
           NONE => NONE
-        | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE)
+        | SOME disk_time => if disk_time <= memory_time then dirty_facts else NONE)
       val (banner, entries) =
         (case dirty_facts' of
           SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
@@ -1278,7 +1278,7 @@
   let
     val hard_timeout = time_mult learn_timeout_slack timeout
     val birth_time = Time.now ()
-    val death_time = Time.+ (birth_time, hard_timeout)
+    val death_time = birth_time + hard_timeout
     val desc = ("Machine learner for Sledgehammer", "")
   in
     Async_Manager_Legacy.thread MaShN birth_time death_time desc task
@@ -1328,7 +1328,7 @@
     learn_timeout facts =
   let
     val timer = Timer.startRealTimer ()
-    fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
+    fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout
 
     val {access_G, ...} = peek_state ctxt
     val is_in_access_G = is_fact_in_graph access_G o snd
@@ -1408,11 +1408,11 @@
               val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
               val learns = (name, parents, feats, deps) :: learns
               val (learns, next_commit) =
-                if Time.> (Timer.checkRealTimer timer, next_commit) then
+                if Timer.checkRealTimer timer > next_commit then
                   (commit false learns [] []; ([], next_commit_time ()))
                 else
                   (learns, next_commit)
-              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+              val timed_out = Timer.checkRealTimer timer > learn_timeout
             in
               (learns, (num_nontrivial, next_commit, timed_out))
             end
@@ -1443,11 +1443,11 @@
                   SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
                 | NONE => (num_nontrivial, relearns, name :: flops))
               val (relearns, flops, next_commit) =
-                if Time.> (Timer.checkRealTimer timer, next_commit) then
+                if Timer.checkRealTimer timer > next_commit then
                   (commit false [] relearns flops; ([], [], next_commit_time ()))
                 else
                   (relearns, flops, next_commit)
-              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+              val timed_out = Timer.checkRealTimer timer > learn_timeout
             in
               ((relearns, flops), (num_nontrivial, next_commit, timed_out))
             end
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -250,7 +250,7 @@
               * 0.001
               |> seconds
             val generous_slice_timeout =
-              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
+              if mode = MaSh then one_day else slice_timeout + atp_timeout_slack
             val _ =
               if debug then
                 quote name ^ " slice #" ^ string_of_int (slice + 1) ^
@@ -328,14 +328,14 @@
         val timer = Timer.startRealTimer ()
 
         fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
-            let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in
-              if Time.<= (time_left, Time.zeroTime) then
+            let val time_left = timeout - Timer.checkRealTimer timer in
+              if time_left <= Time.zeroTime then
                 result
               else
                 run_slice time_left cache slice
                 |> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
                         format_type_enc) =>
-                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome),
+                  (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome),
                    format_type_enc))
             end
           | maybe_run_slice _ result = result
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -130,8 +130,8 @@
 
         val death = Timer.checkRealTimer timer
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
-        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
-        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+        val time_so_far = time_so_far + (death - birth)
+        val timeout = timeout - Timer.checkRealTimer timer
 
         val too_many_facts_perhaps =
           (case outcome of
@@ -143,7 +143,7 @@
           | SOME (SMT_Failure.Other_Failure _) => true)
       in
         if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
-           Time.> (timeout, Time.zeroTime) then
+           timeout > Time.zeroTime then
           let
             val new_num_facts =
               Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
diff -r e6e80a8bf624 -r eb94e570c1a4 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -69,7 +69,7 @@
 
 fun parse_time name s =
   let val secs = if has_junk s then NONE else Real.fromString s in
-    if is_none secs orelse Real.< (the secs, 0.0) then
+    if is_none secs orelse the secs < 0.0 then
       error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
         \(e.g., \"60\", \"0.5\") or \"none\".")
     else
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -52,7 +52,7 @@
   (case Requests.min requests of
     NONE => NONE
   | SOME (time, entries) =>
-      if Time.< (t0, time) then NONE
+      if t0 < time then NONE
       else
         let
           val (rest, (_, event)) = split_last entries;
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -126,7 +126,7 @@
   Multithreading.sync_wait NONE NONE cond lock;
 
 fun wait_timeout timeout cond = (*requires SYNCHRONIZED*)
-  Multithreading.sync_wait NONE (SOME (Time.+ (Time.now (), timeout))) cond lock;
+  Multithreading.sync_wait NONE (SOME (Time.now () + timeout)) cond lock;
 
 fun signal cond = (*requires SYNCHRONIZED*)
   ConditionVar.signal cond;
@@ -280,7 +280,7 @@
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
     val now = Time.now ();
-    val tick = Time.<= (Time.+ (! last_round, next_round), now);
+    val tick = ! last_round + next_round <= now;
     val _ = if tick then last_round := now else ();
 
 
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/Concurrent/mailbox.ML
--- a/src/Pure/Concurrent/mailbox.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/mailbox.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -25,7 +25,7 @@
 
 fun receive timeout (Mailbox mailbox) =
   Synchronized.timed_access mailbox
-    (fn _ => Option.map (fn t => (Time.+ (Time.now (), t))) timeout)
+    (fn _ => Option.map (fn t => Time.now () + t) timeout)
     (fn [] => NONE | msgs => SOME (msgs, []))
   |> these |> rev;
 
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -127,10 +127,10 @@
 fun tracing_time detailed time =
   tracing
    (if not detailed then 5
-    else if Time.>= (time, seconds 1.0) then 1
-    else if Time.>= (time, seconds 0.1) then 2
-    else if Time.>= (time, seconds 0.01) then 3
-    else if Time.>= (time, seconds 0.001) then 4 else 5);
+    else if time >= seconds 1.0 then 1
+    else if time >= seconds 0.1 then 2
+    else if time >= seconds 0.01 then 3
+    else if time >= seconds 0.001 then 4 else 5);
 
 fun real_time f x =
   let
diff -r e6e80a8bf624 -r eb94e570c1a4 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;
 
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -23,7 +23,7 @@
       val start = Time.now ();
 
       val request =
-        Event_Timer.request (Time.+ (start, timeout))
+        Event_Timer.request (start + timeout)
           (fn () => Standard_Thread.interrupt_unsynchronized self);
       val result =
         Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
@@ -33,7 +33,7 @@
       val test = Exn.capture Multithreading.interrupted ();
     in
       if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
-      then raise TIMEOUT (Time.- (stop, start))
+      then raise TIMEOUT (stop - start)
       else (Exn.release test; Exn.release result)
     end);
 
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/General/timing.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -76,7 +76,7 @@
 
 val min_time = Time.fromMilliseconds 1;
 
-fun is_relevant_time time = Time.>= (time, min_time);
+fun is_relevant_time time = time >= min_time;
 
 fun is_relevant {elapsed, cpu, gc} =
   is_relevant_time elapsed orelse
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -651,7 +651,7 @@
     val timings = map get_timing trs;
   in
     if forall is_some timings then
-      SOME (fold (curry Time.+ o the) timings Time.zeroTime)
+      SOME (fold (curry (op +) o the) timings Time.zeroTime)
     else NONE
   end;
 
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -417,7 +417,7 @@
     in
       (case delay of
         NONE => fork ()
-      | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
+      | SOME d => ignore (Event_Timer.request (Time.now () + d) fork))
     end
   else run_process execution_id exec_id print_process;
 
diff -r e6e80a8bf624 -r eb94e570c1a4 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -464,7 +464,7 @@
       val delay = seconds (Options.default_real "editor_execution_delay");
 
       val _ = Future.cancel delay_request;
-      val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
+      val delay_request' = Event_Timer.future (Time.now () + delay);
 
       fun finished_import (name, (node, _)) =
         finished_result node orelse is_some (loaded_theory name);
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