src/Pure/Concurrent/lazy.ML

--- a/src/Pure/Concurrent/lazy.ML	Wed Apr 11 13:37:46 2012 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Wed Apr 11 13:49:09 2012 +0200
@@ -61,15 +61,15 @@
             SOME e =>
               let
                 val res0 = Exn.capture (restore_attributes e) ();
-                val _ = Future.fulfill_result x res0;
-                val res = Future.join_result x;
+                val res1 = Exn.capture (fn () => Future.fulfill_result x res0) ();
+                val res2 = Future.join_result x;
+              in
                 (*semantic race: some other threads might see the same
                   interrupt, until there is a fresh start*)
-                val _ =
-                  if Exn.is_interrupt_exn res then
-                    Synchronized.change var (fn _ => Expr e)
-                  else ();
-              in res end
+                if Exn.is_interrupt_exn res1 orelse Exn.is_interrupt_exn res2 then
+                  (Synchronized.change var (fn _ => Expr e); Exn.interrupt ())
+                else res2
+              end
           | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
         end) ());