src/Pure/System/message_channel.ML
changeset 58857 b0ccc7e1e7f3
parent 57417 29fe9bac501b
child 59058 a78612c67ec0
--- 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;