1.1 --- a/src/Pure/Concurrent/future.ML	Thu Oct 22 15:19:44 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Oct 22 15:21:01 2009 +0200
     1.3 @@ -153,9 +153,7 @@
     1.4              Exn.capture (fn () =>
     1.5                Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) ()
     1.6            else Exn.Exn Exn.Interrupt;
     1.7 -        val _ = Synchronized.change result
     1.8 -          (fn NONE => SOME res
     1.9 -            | SOME _ => raise Fail "Duplicate assignment of future value");
    1.10 +        val _ = Synchronized.assign result (K (SOME res));
    1.11        in
    1.12          (case res of
    1.13            Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
    1.14 @@ -349,8 +347,7 @@
    1.15    | SOME res => res);
    1.16  
    1.17  fun join_wait x =
    1.18 -  Synchronized.guarded_access (result_of x)
    1.19 -    (fn NONE => NONE | some => SOME ((), some));
    1.20 +  Synchronized.readonly_access (result_of x) (fn NONE => NONE | SOME _ => SOME ());
    1.21  
    1.22  fun join_next deps = (*requires SYNCHRONIZED*)
    1.23    if null deps then NONE