Structure Option now declared in MLWorks

--- a/src/Pure/ML-Systems/mlworks.ML	Wed May 27 12:23:45 1998 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Wed May 27 12:25:56 1998 +0200
@@ -25,9 +25,6 @@
 
 (* Poly/ML emulation *)
 
-(*just for versions of MLWorks that don't provide the Option structure*)
-structure Option = General;
-
 (*To exit the system with an exit code -- an alternative to ^D *)
 fun exit 0 = (OS.Process.exit OS.Process.success): unit
   | exit _ = OS.Process.exit OS.Process.failure;