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