src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Sun Aug 25 16:03:12 2013 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun Aug 25 17:04:22 2013 +0200
@@ -535,8 +535,8 @@
   | SOME res =>
       if Exn.is_interrupt_exn res then
         (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
-          NONE => res
-        | SOME exn => Exn.Exn exn)
+          [] => res
+        | exns => Exn.Exn (Par_Exn.make exns))
       else res);
 
 local