# HG changeset patch
# User wenzelm
# Date 1013802224 -3600
# Node ID 4518acda6d93b7a89d2b27aa44fcf11339868c7f
# Parent  d9dd528ecea6a2aa68bbe8eb150baa0e1a581aaa
removed unused unmask_interrupt;

diff -r d9dd528ecea6 -r 4518acda6d93 src/Pure/ML-Systems/mlworks.ML
--- 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;
 
 
diff -r d9dd528ecea6 -r 4518acda6d93 src/Pure/ML-Systems/mosml.ML
--- 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;
 
 
diff -r d9dd528ecea6 -r 4518acda6d93 src/Pure/ML-Systems/polyml-3.x.ML
--- 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;