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;