diff -r 2d16c693d536 -r ef876972fdc1 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Wed Aug 10 14:28:55 2011 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 10 15:17:24 2011 +0200 @@ -247,7 +247,7 @@ val running = Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) (get_tasks groups (group_id group)) []; - val _ = List.app Simple_Thread.interrupt running; + val _ = List.app Simple_Thread.interrupt_unsynchronized running; in null running end; fun cancel_all (Queue {jobs, ...}) = @@ -262,7 +262,7 @@ | _ => (groups, running)) end; val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []); - val _ = List.app Simple_Thread.interrupt running; + val _ = List.app Simple_Thread.interrupt_unsynchronized running; in running_groups end;