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;