| changeset 12896 | 4518acda6d93 |
| parent 12108 | b6f10dcde803 |
| child 12988 | 2112f9e337bb |
--- 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;