--- a/src/Pure/Concurrent/future.ML Wed Oct 17 21:04:51 2012 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Oct 17 21:18:32 2012 +0200
@@ -183,7 +183,9 @@
fun cancel_now group = (*requires SYNCHRONIZED*)
let
val running = Task_Queue.cancel (! queue) group;
- val _ = List.app Simple_Thread.interrupt_unsynchronized running;
+ val _ = running |> List.app (fn thread =>
+ if Simple_Thread.is_self thread then ()
+ else Simple_Thread.interrupt_unsynchronized thread);
in running end;
fun cancel_all () = (*requires SYNCHRONIZED*)