# HG changeset patch
# User wenzelm
# Date 1414792080 -3600
# Node ID b0ccc7e1e7f39a995a99acc7e0b73a4c632244a2
# Parent  4fced55fc5b7c5be0ce7b200527d426506efce5f
tuned;

diff -r 4fced55fc5b7 -r b0ccc7e1e7f3 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Fri Oct 31 22:37:22 2014 +0100
+++ b/src/Pure/System/message_channel.ML	Fri Oct 31 22:48:00 2014 +0100
@@ -51,8 +51,7 @@
         [] => (flush channel; continue NONE)
       | msgs => received timeout msgs)
     and received _ (NONE :: _) = flush channel
-      | received timeout (SOME msg :: rest) =
-          (output_message channel msg; received flush_timeout rest)
+      | received _ (SOME msg :: rest) = (output_message channel msg; received flush_timeout rest)
       | received timeout [] = continue timeout;
   in fn () => continue NONE end;