src/Pure/Concurrent/future.ML
changeset 44247 270366301bd7
parent 44198 a41ea419de68
child 44249 64620f1d6f87
--- a/src/Pure/Concurrent/future.ML	Wed Aug 17 20:08:36 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 17 22:14:22 2011 +0200
@@ -473,9 +473,9 @@
     NONE => Exn.Exn (Fail "Unfinished future")
   | SOME res =>
       if Exn.is_interrupt_exn res then
-        (case Exn.flatten_list (Task_Queue.group_status (Task_Queue.group_of_task (task_of x))) of
-          [] => res
-        | exns => Exn.Exn (Exn.EXCEPTIONS exns))
+        (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
+          NONE => res
+        | SOME exn => Exn.Exn exn)
       else res);
 
 fun join_next deps = (*requires SYNCHRONIZED*)