diff -r 0435d23deccc -r 96cbf4afdc7d src/Pure/Concurrent/mailbox.ML --- a/src/Pure/Concurrent/mailbox.ML Sun Sep 07 22:19:46 2008 +0200 +++ b/src/Pure/Concurrent/mailbox.ML Sun Sep 07 22:19:58 2008 +0200 @@ -53,13 +53,7 @@ ConditionVar.waitUntil (cond, lock, limit) andalso check (); val ok = restore_attributes check () handle Interrupt => (Mutex.unlock lock; raise Interrupt); - val res = - if ok then - let - val (msg, msgs) = Queue.dequeue (! messages); - val _ = messages := msgs; - in SOME msg end - else NONE; + val res = if ok then SOME (change_result messages Queue.dequeue) else NONE; val _ = Mutex.unlock lock; in res end) ();