diff -r 5c9dbd511510 -r 5a07cc86675d src/Pure/ML-Systems/exn.ML --- 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;