exnMessage Interrupt;
authorwenzelm
Mon Nov 09 15:39:31 1998 +0100 (1998-11-09)
changeset 583690f7d9f1a0cc
parent 5835 5b79fbf1a65f
child 5837 ce9a8b05d652
exnMessage Interrupt;
src/Pure/basis.ML
     1.1 --- a/src/Pure/basis.ML	Mon Nov 09 15:38:58 1998 +0100
     1.2 +++ b/src/Pure/basis.ML	Mon Nov 09 15:39:31 1998 +0100
     1.3 @@ -167,7 +167,6 @@
     1.4  in
     1.5    fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure"
     1.6      | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure"
     1.7 -    | exnMessage Interrupt = "Interrupt"
     1.8      | exnMessage (Io msg) = "I/O error: " ^ msg
     1.9      | exnMessage Neg = raised "Neg"
    1.10      | exnMessage Sum = raised "Sum"