src/Pure/ML-Systems/exn.ML
changeset 31427 5a07cc86675d
parent 29564 f8b933a62151
child 32100 8ac6b1102f16
--- a/src/Pure/ML-Systems/exn.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/ML-Systems/exn.ML	Thu Jun 04 17:31:38 2009 +0200
@@ -35,7 +35,7 @@
 fun capture f x = Result (f x) handle e => Exn e;
 
 fun release (Result y) = y
-  | release (Exn e) = raise e;
+  | release (Exn e) = reraise e;
 
 
 (* interrupt and nested exceptions *)
@@ -58,6 +58,6 @@
     | exns => raise EXCEPTIONS exns);
 
 fun release_first results = release_all results
-  handle EXCEPTIONS (exn :: _) => raise exn;
+  handle EXCEPTIONS (exn :: _) => reraise exn;
 
 end;