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