# HG changeset patch
# User wenzelm
# Date 1308863138 -7200
# Node ID 80803078552e0bd34aecad1262233b193239675d
# Parent  6eec653d55993f81f030fc83aed474644c4fc2ee
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);

diff -r 6eec653d5599 -r 80803078552e src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Thu Jun 23 20:30:48 2011 +0200
+++ b/src/Pure/General/exn.ML	Thu Jun 23 23:05:38 2011 +0200
@@ -89,7 +89,8 @@
   else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
 
 fun release_first results = release_all results
-  handle EXCEPTIONS (exn :: _) => reraise exn;
+  handle EXCEPTIONS [] => interrupt ()
+    | EXCEPTIONS (exn :: _) => reraise exn;
 
 end;