Structure Option now declared in MLWorks
authorpaulson
Wed, 27 May 1998 12:25:56 +0200
changeset 4973 7420178bd2d9
parent 4972 7fe1d30c1374
child 4974 45b7a51342a1
Structure Option now declared in MLWorks
src/Pure/ML-Systems/mlworks.ML
--- 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;