author | paulson |
Wed, 27 May 1998 12:25:56 +0200 | |
changeset 4973 | 7420178bd2d9 |
parent 4972 | 7fe1d30c1374 |
child 4974 | 45b7a51342a1 |
--- 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;