# HG changeset patch
# User wenzelm
# Date 1220826334 -7200
# Node ID 8bf8c21296ca1e84bd78771e9c4d483ab026aa27
# Parent  55772e4e95e092ea032fe011f8a7b8998975dd2d
await: SYNCHRONIZED wait!

diff -r 55772e4e95e0 -r 8bf8c21296ca src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Sep 08 00:10:41 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Sep 08 00:25:34 2008 +0200
@@ -190,7 +190,7 @@
 
     fun loop () =
       (case SYNCHRONIZED (fn () => ! r) of
-        NONE => (wait (); loop ())
+        NONE => (SYNCHRONIZED (fn () => wait ()); loop ())
       | SOME res => Exn.release res);
   in loop () end;