removed unused unmask_interrupt;

--- a/src/Pure/ML-Systems/mlworks.ML	Fri Feb 15 20:43:09 2002 +0100
+++ b/src/Pure/ML-Systems/mlworks.ML	Fri Feb 15 20:43:44 2002 +0100
@@ -98,7 +98,6 @@
 MLWorks.Internal.Runtime.Event.interrupt_handler (fn () => raise Interrupt);
 
 fun mask_interrupt f x = f x;           
-fun unmask_interrupt f x = f x;
 fun exhibit_interrupt f x = f x;
 
 

--- a/src/Pure/ML-Systems/mosml.ML	Fri Feb 15 20:43:09 2002 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Fri Feb 15 20:43:44 2002 +0100
@@ -99,7 +99,6 @@
 exception Interrupt;
 
 fun mask_interrupt f x = f x;           
-fun unmask_interrupt f x = f x;
 fun exhibit_interrupt f x = f x;
 
 

--- a/src/Pure/ML-Systems/polyml-3.x.ML	Fri Feb 15 20:43:09 2002 +0100
+++ b/src/Pure/ML-Systems/polyml-3.x.ML	Fri Feb 15 20:43:44 2002 +0100
@@ -85,7 +85,6 @@
 (** interrupts **)      (*Note: may get into race conditions*)
 
 fun mask_interrupt f x = f x;
-fun unmask_interrupt f x = f x;
 fun exhibit_interrupt f x = f x;