# HG changeset patch
# User wenzelm
# Date 910622371 -3600
# Node ID 90f7d9f1a0ccd1da797ad8a50b5f3530d0f7317a
# Parent  5b79fbf1a65f8a1627498d0cb8e47742b2d7e04d
exnMessage Interrupt;

diff -r 5b79fbf1a65f -r 90f7d9f1a0cc src/Pure/basis.ML
--- a/src/Pure/basis.ML	Mon Nov 09 15:38:58 1998 +0100
+++ b/src/Pure/basis.ML	Mon Nov 09 15:39:31 1998 +0100
@@ -167,7 +167,6 @@
 in
   fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure"
     | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure"
-    | exnMessage Interrupt = "Interrupt"
     | exnMessage (Io msg) = "I/O error: " ^ msg
     | exnMessage Neg = raised "Neg"
     | exnMessage Sum = raised "Sum"