src/Pure/Concurrent/event_timer.ML
changeset 62826 eb94e570c1a4
parent 62239 6ee95b93fbed
child 62891 7a11ea5c9626
     1.1 --- a/src/Pure/Concurrent/event_timer.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/event_timer.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    (case Requests.min requests of
     1.5      NONE => NONE
     1.6    | SOME (time, entries) =>
     1.7 -      if Time.< (t0, time) then NONE
     1.8 +      if t0 < time then NONE
     1.9        else
    1.10          let
    1.11            val (rest, (_, event)) = split_last entries;