src/Pure/General/basics.ML
changeset 23358 e0b5a74d7ace
parent 23225 591af6a2f09e
child 23559 0de527730294
--- 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;