# HG changeset patch
# User paulson
# Date 869562914 -7200
# Node ID d4443afc8d289bb1f893fa9b7428461c15349e90
# Parent  ed9de44032e0427a2192fdc2ee55954d5b19c55f
Option is a synonym for General because MLWorks does not yet provide
Option as a separate structure

diff -r ed9de44032e0 -r d4443afc8d28 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;