more robust cancelation, notably of passive futures without scheduler running;

--- 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);