clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);

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