prefer infix operations;
authorwenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826eb94e570c1a4
parent 62825 e6e80a8bf624
child 62827 609f97d79bc2
child 62828 3fee575c9dce
prefer infix operations;
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/Pure/Concurrent/event_timer.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/mailbox.ML
src/Pure/Concurrent/multithreading.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/Concurrent/timeout.ML
src/Pure/General/timing.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4          val facts = named_thms |> map (ref_of_str o fst o fst)
     1.5          val fact_override = {add = facts, del = [], only = true}
     1.6          fun my_timeout time_slice =
     1.7 -          timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
     1.8 +          timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal
     1.9          fun sledge_tac time_slice prover type_enc =
    1.10            Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
    1.11              (override_params prover type_enc (my_timeout time_slice)) fact_override []
     2.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Apr 02 23:14:08 2016 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Apr 02 23:29:05 2016 +0200
     2.3 @@ -989,7 +989,7 @@
     2.4  val fudge_ms = 250
     2.5  
     2.6  fun milliseconds_until_deadline deadline =
     2.7 -  Int.max (0, Time.toMilliseconds (Time.- (deadline, Time.now ())) - fudge_ms)
     2.8 +  Int.max (0, Time.toMilliseconds (deadline - Time.now ()) - fudge_ms)
     2.9  
    2.10  fun uncached_solve_any_problem overlord deadline max_threads max_solutions
    2.11                                 problems =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 02 23:14:08 2016 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 02 23:29:05 2016 +0200
     3.3 @@ -251,7 +251,7 @@
     3.4      fun check_deadline () =
     3.5        let val t = Time.now () in
     3.6          if Time.compare (t, deadline) <> LESS
     3.7 -        then raise Timeout.TIMEOUT (Time.- (t, time_start))
     3.8 +        then raise Timeout.TIMEOUT (t - time_start)
     3.9          else ()
    3.10        end
    3.11  
    3.12 @@ -540,7 +540,7 @@
    3.13          val bit_width = if bits = 0 then 16 else bits + 1
    3.14          val delay =
    3.15            if unsound then
    3.16 -            unsound_delay_for_timeout (Time.- (deadline, Time.now ()))
    3.17 +            unsound_delay_for_timeout (deadline - Time.now ())
    3.18            else
    3.19              0
    3.20          val settings = [("solver", commas_quote kodkod_sat_solver),
    3.21 @@ -986,9 +986,9 @@
    3.22      else
    3.23        let
    3.24          val unknown_outcome = (unknownN, [])
    3.25 -        val deadline = Time.+ (Time.now (), timeout)
    3.26 +        val deadline = Time.now () + timeout
    3.27          val outcome as (outcome_code, _) =
    3.28 -          Timeout.apply (Time.+ (timeout, timeout_bonus))
    3.29 +          Timeout.apply (timeout + timeout_bonus)
    3.30                (pick_them_nits_in_term deadline state params mode i n step subst
    3.31                                        def_assm_ts nondef_assm_ts) orig_t
    3.32            handle TOO_LARGE (_, details) =>
     4.1 --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 02 23:14:08 2016 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 02 23:29:05 2016 +0200
     4.3 @@ -96,7 +96,7 @@
     4.4        let
     4.5          fun time_limit timeout_heap =
     4.6            (case try Thread_Heap.min timeout_heap of
     4.7 -            NONE => Time.+ (Time.now (), max_wait_time)
     4.8 +            NONE => Time.now () + max_wait_time
     4.9            | SOME (time, _) => time)
    4.10  
    4.11          (*action: find threads whose timeout is reached, and interrupt canceling threads*)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Apr 02 23:14:08 2016 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Apr 02 23:29:05 2016 +0200
     5.3 @@ -460,7 +460,7 @@
     5.4  fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
     5.5    (case play of
     5.6      Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
     5.7 -  | Play_Timed_Out time => Time.> (time, Time.zeroTime)
     5.8 +  | Play_Timed_Out time => time > Time.zeroTime
     5.9    | Play_Failed => true)
    5.10  
    5.11  fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sat Apr 02 23:14:08 2016 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sat Apr 02 23:29:05 2016 +0200
     6.3 @@ -103,8 +103,8 @@
     6.4  val merge_slack_factor = 1.5
     6.5  
     6.6  fun adjust_merge_timeout max time =
     6.7 -  let val timeout = time_mult merge_slack_factor (Time.+ (merge_slack_time, time)) in
     6.8 -    if Time.< (max, timeout) then max else timeout
     6.9 +  let val timeout = time_mult merge_slack_factor (merge_slack_time + time) in
    6.10 +    if max < timeout then max else timeout
    6.11    end
    6.12  
    6.13  val compress_degree = 2
    6.14 @@ -171,7 +171,7 @@
    6.15                val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment)
    6.16  
    6.17                (* check if the modified step can be preplayed fast enough *)
    6.18 -              val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
    6.19 +              val timeout = adjust_merge_timeout preplay_timeout (time + reference_time l')
    6.20              in
    6.21                (case preplay_isar_step ctxt [] timeout hopeless step'' of
    6.22                  meths_outcomes as (_, Played time'') :: _ =>
    6.23 @@ -215,7 +215,7 @@
    6.24                | SOME times0 =>
    6.25                  let
    6.26                    val n = length labels
    6.27 -                  val total_time = Library.foldl Time.+ (reference_time l, times0)
    6.28 +                  val total_time = Library.foldl (op +) (reference_time l, times0)
    6.29                    val timeout = adjust_merge_timeout preplay_timeout
    6.30                      (Time.fromReal (Time.toReal total_time / Real.fromInt n))
    6.31                    val meths_outcomess =
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sat Apr 02 23:14:08 2016 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sat Apr 02 23:29:05 2016 +0200
     7.3 @@ -45,7 +45,7 @@
     7.4  
     7.5      fun minimize_half _ min_facts [] time = (min_facts, time)
     7.6        | minimize_half mk_step min_facts (fact :: facts) time =
     7.7 -        (case preplay_isar_step_for_method ctxt [] (Time.+ (time, slack)) meth
     7.8 +        (case preplay_isar_step_for_method ctxt [] (time + slack) meth
     7.9              (mk_step (min_facts @ facts)) of
    7.10            Played time' => minimize_half mk_step min_facts facts time'
    7.11          | _ => minimize_half mk_step (fact :: min_facts) facts time)
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:14:08 2016 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:29:05 2016 +0200
     8.3 @@ -52,7 +52,7 @@
     8.4  
     8.5        fun apply_f x =
     8.6          let val timeout = !next_timeout in
     8.7 -          if Time.<= (timeout, min_timeout) then
     8.8 +          if timeout <= min_timeout then
     8.9              NONE
    8.10            else
    8.11              let val y = f timeout x in
    8.12 @@ -188,7 +188,7 @@
    8.13  
    8.14  fun add_preplay_outcomes Play_Failed _ = Play_Failed
    8.15    | add_preplay_outcomes _ Play_Failed = Play_Failed
    8.16 -  | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
    8.17 +  | add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2)
    8.18    | add_preplay_outcomes play1 play2 =
    8.19      Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2)))
    8.20  
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Apr 02 23:14:08 2016 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Apr 02 23:29:05 2016 +0200
     9.3 @@ -168,7 +168,7 @@
     9.4  
     9.5  fun normalize_scores _ [] = []
     9.6    | normalize_scores max_facts xs =
     9.7 -    map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
     9.8 +    map (apsnd (curry (op *) (1.0 / avg (map snd (take max_facts xs))))) xs
     9.9  
    9.10  fun mesh_facts maybe_distinct _ max_facts [(_, (sels, unks))] =
    9.11      map fst (take max_facts sels) @ take (max_facts - length sels) unks
    9.12 @@ -655,7 +655,7 @@
    9.13      (case try OS.FileSys.modTime (File.platform_path path) of
    9.14        NONE => time_state
    9.15      | SOME disk_time =>
    9.16 -      if Time.>= (memory_time, disk_time) then
    9.17 +      if memory_time >= disk_time then
    9.18          time_state
    9.19        else
    9.20          (disk_time,
    9.21 @@ -700,7 +700,7 @@
    9.22        val dirty_facts' =
    9.23          (case try OS.FileSys.modTime (File.platform_path path) of
    9.24            NONE => NONE
    9.25 -        | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE)
    9.26 +        | SOME disk_time => if disk_time <= memory_time then dirty_facts else NONE)
    9.27        val (banner, entries) =
    9.28          (case dirty_facts' of
    9.29            SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
    9.30 @@ -1278,7 +1278,7 @@
    9.31    let
    9.32      val hard_timeout = time_mult learn_timeout_slack timeout
    9.33      val birth_time = Time.now ()
    9.34 -    val death_time = Time.+ (birth_time, hard_timeout)
    9.35 +    val death_time = birth_time + hard_timeout
    9.36      val desc = ("Machine learner for Sledgehammer", "")
    9.37    in
    9.38      Async_Manager_Legacy.thread MaShN birth_time death_time desc task
    9.39 @@ -1328,7 +1328,7 @@
    9.40      learn_timeout facts =
    9.41    let
    9.42      val timer = Timer.startRealTimer ()
    9.43 -    fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
    9.44 +    fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout
    9.45  
    9.46      val {access_G, ...} = peek_state ctxt
    9.47      val is_in_access_G = is_fact_in_graph access_G o snd
    9.48 @@ -1408,11 +1408,11 @@
    9.49                val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
    9.50                val learns = (name, parents, feats, deps) :: learns
    9.51                val (learns, next_commit) =
    9.52 -                if Time.> (Timer.checkRealTimer timer, next_commit) then
    9.53 +                if Timer.checkRealTimer timer > next_commit then
    9.54                    (commit false learns [] []; ([], next_commit_time ()))
    9.55                  else
    9.56                    (learns, next_commit)
    9.57 -              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
    9.58 +              val timed_out = Timer.checkRealTimer timer > learn_timeout
    9.59              in
    9.60                (learns, (num_nontrivial, next_commit, timed_out))
    9.61              end
    9.62 @@ -1443,11 +1443,11 @@
    9.63                    SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
    9.64                  | NONE => (num_nontrivial, relearns, name :: flops))
    9.65                val (relearns, flops, next_commit) =
    9.66 -                if Time.> (Timer.checkRealTimer timer, next_commit) then
    9.67 +                if Timer.checkRealTimer timer > next_commit then
    9.68                    (commit false [] relearns flops; ([], [], next_commit_time ()))
    9.69                  else
    9.70                    (relearns, flops, next_commit)
    9.71 -              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
    9.72 +              val timed_out = Timer.checkRealTimer timer > learn_timeout
    9.73              in
    9.74                ((relearns, flops), (num_nontrivial, next_commit, timed_out))
    9.75              end
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Apr 02 23:14:08 2016 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Apr 02 23:29:05 2016 +0200
    10.3 @@ -250,7 +250,7 @@
    10.4                * 0.001
    10.5                |> seconds
    10.6              val generous_slice_timeout =
    10.7 -              if mode = MaSh then one_day else Time.+ (slice_timeout, atp_timeout_slack)
    10.8 +              if mode = MaSh then one_day else slice_timeout + atp_timeout_slack
    10.9              val _ =
   10.10                if debug then
   10.11                  quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   10.12 @@ -328,14 +328,14 @@
   10.13          val timer = Timer.startRealTimer ()
   10.14  
   10.15          fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
   10.16 -            let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in
   10.17 -              if Time.<= (time_left, Time.zeroTime) then
   10.18 +            let val time_left = timeout - Timer.checkRealTimer timer in
   10.19 +              if time_left <= Time.zeroTime then
   10.20                  result
   10.21                else
   10.22                  run_slice time_left cache slice
   10.23                  |> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
   10.24                          format_type_enc) =>
   10.25 -                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome),
   10.26 +                  (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome),
   10.27                     format_type_enc))
   10.28              end
   10.29            | maybe_run_slice _ result = result
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sat Apr 02 23:14:08 2016 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sat Apr 02 23:29:05 2016 +0200
    11.3 @@ -130,8 +130,8 @@
    11.4  
    11.5          val death = Timer.checkRealTimer timer
    11.6          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    11.7 -        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
    11.8 -        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
    11.9 +        val time_so_far = time_so_far + (death - birth)
   11.10 +        val timeout = timeout - Timer.checkRealTimer timer
   11.11  
   11.12          val too_many_facts_perhaps =
   11.13            (case outcome of
   11.14 @@ -143,7 +143,7 @@
   11.15            | SOME (SMT_Failure.Other_Failure _) => true)
   11.16        in
   11.17          if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
   11.18 -           Time.> (timeout, Time.zeroTime) then
   11.19 +           timeout > Time.zeroTime then
   11.20            let
   11.21              val new_num_facts =
   11.22                Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Apr 02 23:14:08 2016 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Apr 02 23:29:05 2016 +0200
    12.3 @@ -69,7 +69,7 @@
    12.4  
    12.5  fun parse_time name s =
    12.6    let val secs = if has_junk s then NONE else Real.fromString s in
    12.7 -    if is_none secs orelse Real.< (the secs, 0.0) then
    12.8 +    if is_none secs orelse the secs < 0.0 then
    12.9        error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \
   12.10          \(e.g., \"60\", \"0.5\") or \"none\".")
   12.11      else
    13.1 --- a/src/Pure/Concurrent/event_timer.ML	Sat Apr 02 23:14:08 2016 +0200
    13.2 +++ b/src/Pure/Concurrent/event_timer.ML	Sat Apr 02 23:29:05 2016 +0200
    13.3 @@ -52,7 +52,7 @@
    13.4    (case Requests.min requests of
    13.5      NONE => NONE
    13.6    | SOME (time, entries) =>
    13.7 -      if Time.< (t0, time) then NONE
    13.8 +      if t0 < time then NONE
    13.9        else
   13.10          let
   13.11            val (rest, (_, event)) = split_last entries;
    14.1 --- a/src/Pure/Concurrent/future.ML	Sat Apr 02 23:14:08 2016 +0200
    14.2 +++ b/src/Pure/Concurrent/future.ML	Sat Apr 02 23:29:05 2016 +0200
    14.3 @@ -126,7 +126,7 @@
    14.4    Multithreading.sync_wait NONE NONE cond lock;
    14.5  
    14.6  fun wait_timeout timeout cond = (*requires SYNCHRONIZED*)
    14.7 -  Multithreading.sync_wait NONE (SOME (Time.+ (Time.now (), timeout))) cond lock;
    14.8 +  Multithreading.sync_wait NONE (SOME (Time.now () + timeout)) cond lock;
    14.9  
   14.10  fun signal cond = (*requires SYNCHRONIZED*)
   14.11    ConditionVar.signal cond;
   14.12 @@ -280,7 +280,7 @@
   14.13  fun scheduler_next () = (*requires SYNCHRONIZED*)
   14.14    let
   14.15      val now = Time.now ();
   14.16 -    val tick = Time.<= (Time.+ (! last_round, next_round), now);
   14.17 +    val tick = ! last_round + next_round <= now;
   14.18      val _ = if tick then last_round := now else ();
   14.19  
   14.20  
    15.1 --- a/src/Pure/Concurrent/mailbox.ML	Sat Apr 02 23:14:08 2016 +0200
    15.2 +++ b/src/Pure/Concurrent/mailbox.ML	Sat Apr 02 23:29:05 2016 +0200
    15.3 @@ -25,7 +25,7 @@
    15.4  
    15.5  fun receive timeout (Mailbox mailbox) =
    15.6    Synchronized.timed_access mailbox
    15.7 -    (fn _ => Option.map (fn t => (Time.+ (Time.now (), t))) timeout)
    15.8 +    (fn _ => Option.map (fn t => Time.now () + t) timeout)
    15.9      (fn [] => NONE | msgs => SOME (msgs, []))
   15.10    |> these |> rev;
   15.11  
    16.1 --- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 02 23:14:08 2016 +0200
    16.2 +++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 02 23:29:05 2016 +0200
    16.3 @@ -127,10 +127,10 @@
    16.4  fun tracing_time detailed time =
    16.5    tracing
    16.6     (if not detailed then 5
    16.7 -    else if Time.>= (time, seconds 1.0) then 1
    16.8 -    else if Time.>= (time, seconds 0.1) then 2
    16.9 -    else if Time.>= (time, seconds 0.01) then 3
   16.10 -    else if Time.>= (time, seconds 0.001) then 4 else 5);
   16.11 +    else if time >= seconds 1.0 then 1
   16.12 +    else if time >= seconds 0.1 then 2
   16.13 +    else if time >= seconds 0.01 then 3
   16.14 +    else if time >= seconds 0.001 then 4 else 5);
   16.15  
   16.16  fun real_time f x =
   16.17    let
    17.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 23:14:08 2016 +0200
    17.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 23:29:05 2016 +0200
    17.3 @@ -139,7 +139,7 @@
    17.4      let
    17.5        val start = Time.now ();
    17.6        val result = Exn.capture (restore_attributes e) ();
    17.7 -      val t = Time.- (Time.now (), start);
    17.8 +      val t = Time.now () - start;
    17.9        val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
   17.10      in Exn.release result end) ();
   17.11  
   17.12 @@ -167,14 +167,14 @@
   17.13  (* timing *)
   17.14  
   17.15  fun running task =
   17.16 -  update_timing (fn t => fn (a, b, ds) => (Time.+ (a, t), b, ds)) task;
   17.17 +  update_timing (fn t => fn (a, b, ds) => (a + t, b, ds)) task;
   17.18  
   17.19  fun joining task =
   17.20 -  update_timing (fn t => fn (a, b, ds) => (Time.- (a, t), b, ds)) task;
   17.21 +  update_timing (fn t => fn (a, b, ds) => (a - t, b, ds)) task;
   17.22  
   17.23  fun waiting task deps =
   17.24    update_timing (fn t => fn (a, b, ds) =>
   17.25 -    (Time.- (a, t), Time.+ (b, t),
   17.26 +    (a - t, b + t,
   17.27        if ! Multithreading.trace > 0
   17.28        then fold (insert (op =) o name_of_task) deps ds else ds)) task;
   17.29  
    18.1 --- a/src/Pure/Concurrent/timeout.ML	Sat Apr 02 23:14:08 2016 +0200
    18.2 +++ b/src/Pure/Concurrent/timeout.ML	Sat Apr 02 23:29:05 2016 +0200
    18.3 @@ -23,7 +23,7 @@
    18.4        val start = Time.now ();
    18.5  
    18.6        val request =
    18.7 -        Event_Timer.request (Time.+ (start, timeout))
    18.8 +        Event_Timer.request (start + timeout)
    18.9            (fn () => Standard_Thread.interrupt_unsynchronized self);
   18.10        val result =
   18.11          Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
   18.12 @@ -33,7 +33,7 @@
   18.13        val test = Exn.capture Multithreading.interrupted ();
   18.14      in
   18.15        if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
   18.16 -      then raise TIMEOUT (Time.- (stop, start))
   18.17 +      then raise TIMEOUT (stop - start)
   18.18        else (Exn.release test; Exn.release result)
   18.19      end);
   18.20  
    19.1 --- a/src/Pure/General/timing.ML	Sat Apr 02 23:14:08 2016 +0200
    19.2 +++ b/src/Pure/General/timing.ML	Sat Apr 02 23:29:05 2016 +0200
    19.3 @@ -76,7 +76,7 @@
    19.4  
    19.5  val min_time = Time.fromMilliseconds 1;
    19.6  
    19.7 -fun is_relevant_time time = Time.>= (time, min_time);
    19.8 +fun is_relevant_time time = time >= min_time;
    19.9  
   19.10  fun is_relevant {elapsed, cpu, gc} =
   19.11    is_relevant_time elapsed orelse
    20.1 --- a/src/Pure/Isar/toplevel.ML	Sat Apr 02 23:14:08 2016 +0200
    20.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Apr 02 23:29:05 2016 +0200
    20.3 @@ -651,7 +651,7 @@
    20.4      val timings = map get_timing trs;
    20.5    in
    20.6      if forall is_some timings then
    20.7 -      SOME (fold (curry Time.+ o the) timings Time.zeroTime)
    20.8 +      SOME (fold (curry (op +) o the) timings Time.zeroTime)
    20.9      else NONE
   20.10    end;
   20.11  
    21.1 --- a/src/Pure/PIDE/command.ML	Sat Apr 02 23:14:08 2016 +0200
    21.2 +++ b/src/Pure/PIDE/command.ML	Sat Apr 02 23:29:05 2016 +0200
    21.3 @@ -417,7 +417,7 @@
    21.4      in
    21.5        (case delay of
    21.6          NONE => fork ()
    21.7 -      | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
    21.8 +      | SOME d => ignore (Event_Timer.request (Time.now () + d) fork))
    21.9      end
   21.10    else run_process execution_id exec_id print_process;
   21.11  
    22.1 --- a/src/Pure/PIDE/document.ML	Sat Apr 02 23:14:08 2016 +0200
    22.2 +++ b/src/Pure/PIDE/document.ML	Sat Apr 02 23:29:05 2016 +0200
    22.3 @@ -464,7 +464,7 @@
    22.4        val delay = seconds (Options.default_real "editor_execution_delay");
    22.5  
    22.6        val _ = Future.cancel delay_request;
    22.7 -      val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
    22.8 +      val delay_request' = Event_Timer.future (Time.now () + delay);
    22.9  
   22.10        fun finished_import (name, (node, _)) =
   22.11          finished_result node orelse is_some (loaded_theory name);
    23.1 --- a/src/Pure/Tools/build.ML	Sat Apr 02 23:14:08 2016 +0200
    23.2 +++ b/src/Pure/Tools/build.ML	Sat Apr 02 23:29:05 2016 +0200
    23.3 @@ -22,7 +22,7 @@
    23.4    (case Markup.parse_command_timing_properties props of
    23.5      SOME ({file, offset, name}, time) =>
    23.6        Symtab.map_default (file, Inttab.empty)
    23.7 -        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
    23.8 +        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
    23.9    | NONE => I);
   23.10  
   23.11  fun approximative_id name pos =
   23.12 @@ -83,7 +83,7 @@
   23.13            val {elapsed, ...} = Markup.parse_timing_properties args;
   23.14            val is_significant =
   23.15              Timing.is_relevant_time elapsed andalso
   23.16 -            Time.>= (elapsed, Options.default_seconds "command_timing_threshold");
   23.17 +            elapsed >= Options.default_seconds "command_timing_threshold";
   23.18          in
   23.19            if is_significant then
   23.20              (case approximative_id name pos of