src/Pure/basis.ML
changeset 5836 90f7d9f1a0cc
parent 5643 983ce1421211
child 11852 a528a716a312
     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"