author | wenzelm |
Mon, 09 Nov 1998 15:39:31 +0100 | |
changeset 5836 | 90f7d9f1a0cc |
parent 5835 | 5b79fbf1a65f |
child 5837 | ce9a8b05d652 |
src/Pure/basis.ML | file | annotate | diff | comparison | revisions |
--- 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"