--- 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;