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;