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