simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
clarified Task_Queue.group_status;
tuned;

--- 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

--- a/src/Pure/Concurrent/task_queue.ML	Sun Aug 25 16:03:12 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sun Aug 25 17:04:22 2013 +0200
@@ -12,7 +12,7 @@
   val eq_group: group * group -> bool
   val cancel_group: group -> exn -> unit
   val is_canceled: group -> bool
-  val group_status: group -> exn option
+  val group_status: group -> exn list
   val str_of_group: group -> string
   val str_of_groups: group -> string
   type task
@@ -82,14 +82,9 @@
   is_some (Synchronized.value status) orelse
     (case parent of NONE => false | SOME group => is_canceled group);
 
-fun group_exns (Group {parent, status, ...}) =
+fun group_status (Group {parent, status, ...}) =
   the_list (Synchronized.value status) @
-    (case parent of NONE => [] | SOME group => group_exns group);
-
-fun group_status group =
-  (case group_exns group of
-    [] => NONE
-  | exns => SOME (Par_Exn.make exns));
+    (case parent of NONE => [] | SOME group => group_status group);
 
 fun str_of_group group =
   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));

--- a/src/Pure/Thy/thy_info.ML	Sun Aug 25 16:03:12 2013 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Aug 25 17:04:22 2013 +0200
@@ -174,11 +174,9 @@
 fun result_commit (Result {commit, ...}) = commit;
 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
 
-fun join_proofs (Result {theory, id, ...}) =
-  let
-    val result1 = Exn.capture Thm.join_theory_proofs theory;
-    val results2 = Future.join_results (Goal.peek_futures id);
-  in result1 :: results2 end;
+fun join_theory (Result {theory, id, ...}) =
+  Exn.capture Thm.join_theory_proofs theory ::
+  map Exn.Exn (maps Task_Queue.group_status (Goal.peek_futures id));
 
 
 datatype task =
@@ -198,7 +196,7 @@
       Task (parents, body) =>
         let
           val result = body (task_parents deps parents);
-          val _ = Par_Exn.release_all (join_proofs result);
+          val _ = Par_Exn.release_all (join_theory result);
           val _ = result_present result ();
           val _ = result_commit result ();
         in result_theory result end
@@ -224,7 +222,7 @@
     val results1 = futures
       |> maps (fn future =>
           (case Future.join_result future of
-            Exn.Res result => join_proofs result
+            Exn.Res result => join_theory result
           | Exn.Exn exn => [Exn.Exn exn]));
 
     val results2 = futures
@@ -237,7 +235,7 @@
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
     (* FIXME avoid global reset_futures (!??) *)
-    val results4 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ()));
+    val results4 = map Exn.Exn (maps Task_Queue.group_status (Goal.reset_futures ()));
 
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in () end);

--- a/src/Pure/goal.ML	Sun Aug 25 16:03:12 2013 +0200
+++ b/src/Pure/goal.ML	Sun Aug 25 17:04:22 2013 +0200
@@ -26,7 +26,7 @@
   val norm_result: thm -> thm
   val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
   val fork: int -> (unit -> 'a) -> 'a future
-  val peek_futures: int -> unit future list
+  val peek_futures: int -> Future.group list
   val purge_futures: int list -> unit
   val reset_futures: unit -> Future.group list
   val shutdown_futures: unit -> unit
@@ -117,12 +117,11 @@
 
 val forked_proofs =
   Synchronized.var "forked_proofs"
-    (Inttab.empty: (Future.group * unit future) list Inttab.table);
+    (Inttab.empty: Future.group list Inttab.table);
 
 fun register_forked id future =
-  Synchronized.change forked_proofs (fn tab =>
-    let val group = Task_Queue.group_of_task (Future.task_of future)
-    in Inttab.cons_list (id, (group, Future.map (K ()) future)) tab end);
+  Synchronized.change forked_proofs
+    (Inttab.cons_list (id, Task_Queue.group_of_task (Future.task_of future)));
 
 fun status task markups =
   let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
@@ -164,30 +163,28 @@
   fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e;
 
 fun peek_futures id =
-  map #2 (Inttab.lookup_list (Synchronized.value forked_proofs) id);
-
-fun check_canceled id group =
-  if Task_Queue.is_canceled group then ()
-  else raise Fail ("Attempt to purge valid execution " ^ string_of_int id);
+  Inttab.lookup_list (Synchronized.value forked_proofs) id;
 
 fun purge_futures ids =
   Synchronized.change forked_proofs (fn tab =>
     let
       val tab' = fold Inttab.delete_safe ids tab;
       val () =
-        Inttab.fold (fn (id, futures) => fn () =>
+        Inttab.fold (fn (id, groups) => fn () =>
           if Inttab.defined tab' id then ()
-          else List.app (check_canceled id o #1) futures) tab ();
+          else groups |> List.app (fn group =>
+            if Task_Queue.is_canceled group then ()
+            else raise Fail ("Attempt to purge valid execution " ^ string_of_int id))) tab ();
     in tab' end);
 
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn tab =>
-    let val groups = Inttab.fold (fold (cons o #1) o #2) tab []
+    let val groups = Inttab.fold (fold cons o #2) tab []
     in (groups, Inttab.empty) end);
 
 fun shutdown_futures () =
   (Future.shutdown ();
-    (case map_filter Task_Queue.group_status (reset_futures ()) of
+    (case maps Task_Queue.group_status (reset_futures ()) of
       [] => ()
     | exns => raise Par_Exn.make exns));