Option is a synonym for General because MLWorks does not yet provide
authorpaulson
Tue, 22 Jul 1997 11:15:14 +0200
changeset 3539 d4443afc8d28
parent 3538 ed9de44032e0
child 3540 acd60238f191
Option is a synonym for General because MLWorks does not yet provide Option as a separate structure
src/Pure/ML-Systems/MLWorks.ML
--- a/src/Pure/ML-Systems/MLWorks.ML	Tue Jul 22 11:14:18 1997 +0200
+++ b/src/Pure/ML-Systems/MLWorks.ML	Tue Jul 22 11:15:14 1997 +0200
@@ -25,6 +25,8 @@
 **)
 
 
+structure Option = General;
+
 (*To exit the system with an exit code -- an alternative to ^D *)
 fun exit 0 = OS.Process.exit OS.Process.success
   | exit _ = OS.Process.exit OS.Process.failure;