diff -r 16e0ec4bcd81 -r e0b5a74d7ace src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Wed Jun 13 00:02:00 2007 +0200
+++ b/src/Pure/General/basics.ML	Wed Jun 13 00:02:01 2007 +0200
@@ -94,8 +94,6 @@
 
 (* partiality *)
 
-exception Interrupt = Interrupt;   (*signals intruding execution :-[*)
-
 fun try f x = SOME (f x)
   handle Interrupt => raise Interrupt | _ => NONE;