author | wenzelm |
Thu, 08 Aug 2002 23:53:22 +0200 | |
changeset 13488 | a246d390f033 |
parent 13487 | 1291c6375c29 |
child 13489 | 79d117a158bd |
--- 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;