# HG changeset patch
# User wenzelm
# Date 1418391033 -3600
# Node ID 853a8cb902aa7ac3648cbf82ca98e655172b45ce
# Parent  fd748d770770b495a1c3e089078f950ae67bc3a8
tuned;

diff -r fd748d770770 -r 853a8cb902aa src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Dec 11 23:42:03 2014 +0100
+++ b/src/Doc/Implementation/ML.thy	Fri Dec 12 14:30:33 2014 +0100
@@ -2019,8 +2019,8 @@
   individual exceptions by conventional @{verbatim "handle"} of ML.
 
   \item @{ML Par_Exn.release_first} is similar to @{ML
-  Par_Exn.release_all}, but only the first exception that has occurred
-  in the original evaluation process is raised again, the others are
+  Par_Exn.release_all}, but only the first (meaningful) exception that has
+  occurred in the original evaluation process is raised again, the others are
   ignored.  That single exception may get handled by conventional
   means in ML.
 
diff -r fd748d770770 -r 853a8cb902aa src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Thu Dec 11 23:42:03 2014 +0100
+++ b/src/Pure/General/exn.scala	Fri Dec 12 14:30:33 2014 +0100
@@ -27,13 +27,10 @@
     }
 
   def release_first[A](results: List[Result[A]]): List[A] =
-    if (results.forall({ case Res(_) => true case _ => false }))
-      results.map(release(_))
-    else
-      results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
-        case Some(Exn(exn)) => throw exn
-        case _ => results match { case Exn(exn) :: _ => throw exn case _ => ??? }
-      }
+    results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
+      case Some(Exn(exn)) => throw exn
+      case _ => results.map(release(_))
+    }
 
 
   /* interrupts */