src/Pure/ML-Systems/smlnj.ML
changeset 28443 de653f1ad78b
parent 28284 2161665a0a5d
child 28488 18fea7e88ea1
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Oct 01 12:00:01 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Oct 01 12:00:02 2008 +0200
     1.3 @@ -4,6 +4,8 @@
     1.4  Compatibility file for Standard ML of New Jersey 110 or later.
     1.5  *)
     1.6  
     1.7 +exception Interrupt;
     1.8 +
     1.9  use "ML-Systems/proper_int.ML";
    1.10  use "ML-Systems/overloading_smlnj.ML";
    1.11  use "ML-Systems/exn.ML";
    1.12 @@ -145,8 +147,6 @@
    1.13  
    1.14  (** interrupts **)
    1.15  
    1.16 -exception Interrupt;
    1.17 -
    1.18  local
    1.19  
    1.20  fun change_signal new_handler f x =