diff -r fa094e173cb9 -r 7449b804073b src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Fri Aug 31 22:34:37 2012 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Sat Sep 01 19:27:28 2012 +0200
@@ -10,6 +10,7 @@
   val serial: exn -> serial * exn
   val make: exn list -> exn
   val dest: exn -> exn list option
+  val is_interrupted: 'a Exn.result list -> bool
   val release_all: 'a Exn.result list -> 'a list
   val release_first: 'a Exn.result list -> 'a list
 end;
@@ -53,6 +54,10 @@
 
 (* parallel results *)
 
+fun is_interrupted results =
+  exists (fn Exn.Exn _ => true | _ => false) results andalso
+    Exn.is_interrupt (make (map_filter Exn.get_exn results));
+
 fun release_all results =
   if forall (fn Exn.Res _ => true | _ => false) results
   then map Exn.release results