# HG changeset patch
# User wenzelm
# Date 1028843602 -7200
# Node ID a246d390f0330f39ab0145925f1ea51283560d3c
# Parent  1291c6375c29bf68d33a899aee9ec7d4cf4ffee4
transform_error: pass through Interrupt;

diff -r 1291c6375c29 -r a246d390f033 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Aug 08 23:52:55 2002 +0200
+++ b/src/Pure/library.ML	Thu Aug 08 23:53:22 2002 +0200
@@ -1213,7 +1213,7 @@
 (* transform any exception, including ERROR *)
 
 fun transform_failure exn f x =
-  transform_error f x handle e => raise exn e;
+  transform_error f x handle Interrupt => raise Interrupt | e => raise exn e;