diff -r 16bf3e9786a3 -r eedea6f0b37e src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Jan 06 18:14:16 2010 +0100 +++ b/src/Pure/Concurrent/future.ML Wed Jan 06 18:22:43 2010 +0100 @@ -505,7 +505,8 @@ else interruptible f x; (*cancel: present and future group members will be interrupted eventually*) -fun cancel_group group = SYNCHRONIZED "cancel" (fn () => cancel_later group); +fun cancel_group group = + SYNCHRONIZED "cancel" (fn () => if cancel_now group then () else cancel_later group); fun cancel x = cancel_group (group_of x);