--- a/src/Pure/Concurrent/task_queue.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Thu Sep 09 17:20:27 2010 +0200
@@ -80,9 +80,8 @@
fun cancel_group (Group {status, ...}) exn =
Synchronized.change status
(fn exns =>
- (case exn of
- Exn.Interrupt => if null exns then [exn] else exns
- | _ => exn :: exns));
+ if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
+ else exns);
fun is_canceled (Group {parent, status, ...}) =
not (null (Synchronized.value status)) orelse