src/Pure/ML-Systems/mlworks.ML
changeset 4973 7420178bd2d9
parent 4430 b2c1cf960c53
child 4977 6cec2c0ffdbf
--- 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;