# HG changeset patch
# User paulson
# Date 896264756 -7200
# Node ID 7420178bd2d9e2628ccc0eb056d4cf27fd78d951
# Parent  7fe1d30c13740c6ccc85dbac2e3da0d8760faacf
Structure Option now declared in MLWorks

diff -r 7fe1d30c1374 -r 7420178bd2d9 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;