# HG changeset patch
# User wenzelm
# Date 1550667532 -3600
# Node ID 93784805c6c5e604bcb02786374b5b6ead03152d
# Parent  8c587dd44f51e67e1314b5fffe731f0baa8ca3a5
tuned;

diff -r 8c587dd44f51 -r 93784805c6c5 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Wed Feb 20 12:10:40 2019 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Wed Feb 20 13:58:52 2019 +0100
@@ -48,17 +48,18 @@
 fun next_request_time (requests: requests) =
   Option.map fst (Requests.min requests);
 
-fun next_request_event t0 (requests: requests) =
+fun next_request_event time (requests: requests) =
   (case Requests.min requests of
     NONE => NONE
-  | SOME (time, entries) =>
-      if t0 < time then NONE
+  | SOME (request_time, entries) =>
+      if time < request_time then NONE
       else
         let
           val (rest, (_, event)) = split_last entries;
           val requests' =
-            if null rest then Requests.delete time requests
-            else Requests.update (time, rest) requests;
+            if null rest
+            then Requests.delete request_time requests
+            else Requests.update (request_time, rest) requests;
         in SOME (event, requests') end);