clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;

--- a/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:14:22 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Wed Aug 17 22:25:00 2011 +0200
@@ -42,8 +42,13 @@
   if all_res results then map Exn.release results
   else raise make (map_filter Exn.get_exn results);
 
-fun release_first results = release_all results
-  handle Par_Exn ((serial, exn) :: _) => reraise exn;  (* FIXME preserve serial in location (?!?) *)
+fun release_first results =
+  if all_res results then map Exn.release results
+  else
+    (case get_first
+        (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
+      NONE => Exn.interrupt ()
+    | SOME exn => reraise exn);
 
 end;