1.1 --- a/src/Pure/Concurrent/future.ML	Wed Aug 10 14:04:45 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Aug 10 14:28:55 2011 +0200
     1.3 @@ -197,6 +197,7 @@
     1.4      val _ = SYNCHRONIZED "finish" (fn () =>
     1.5        let
     1.6          val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
     1.7 +        val _ = Exn.capture Multithreading.interrupted ();
     1.8          val _ =
     1.9            if ok then ()
    1.10            else if cancel_now group then ()
    1.11 @@ -397,7 +398,8 @@
    1.12          | _ => reraise exn);
    1.13      val ok =
    1.14        (case the (Single_Assignment.peek result) of
    1.15 -        Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
    1.16 +        Exn.Exn exn =>
    1.17 +          (SYNCHRONIZED "cancel" (fn () => Task_Queue.cancel_group group exn); false)
    1.18        | Exn.Res _ => true);
    1.19    in ok end;
    1.20