diff -r 8a1ab91df301 -r 05514b09bb4b src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 17:27:18 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Feb 08 17:36:21 2011 +0100
@@ -73,36 +73,6 @@
 
 
 
-(** interrupts **)
-
-local
-
-val sig_int = 2;
-val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
-
-val _ = Signal.signal (sig_int, default_handler);
-val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
-
-fun change_signal new_handler f x =
-  let
-    (*RACE wrt. other signals!*)
-    val old_handler = Signal.signal (sig_int, new_handler);
-    val result = Exn.capture (f old_handler) x;
-    val _ = Signal.signal (sig_int, old_handler);
-  in Exn.release result end;
-
-in
-
-fun interruptible f = change_signal default_handler (fn _ => f);
-
-fun uninterruptible f =
-  change_signal Signal.SIG_IGN
-    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
-
-end;
-
-
-
 (** OS related **)
 
 (* current directory *)