src/Pure/Concurrent/event_timer.ML
changeset 62239 6ee95b93fbed
parent 61556 0d4ee4168e41
child 62826 eb94e570c1a4
--- a/src/Pure/Concurrent/event_timer.ML	Sun Jan 24 14:57:42 2016 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Sun Jan 24 14:58:56 2016 +0100
@@ -110,7 +110,7 @@
 
 fun shutdown () =
   uninterruptible (fn restore_attributes => fn () =>
-    if Synchronized.change_result state (fn st as State {requests, status, manager} =>
+    if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
       if is_shutdown Normal st then (false, st)
       else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
         raise Fail "Concurrent attempt to shutdown event timer"