exnMessage Interrupt;
authorwenzelm
Mon, 09 Nov 1998 15:39:31 +0100
changeset 5836 90f7d9f1a0cc
parent 5835 5b79fbf1a65f
child 5837 ce9a8b05d652
exnMessage Interrupt;
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"