open General (type option is in Option in the newer versions, but always
authorwenzelm
Thu, 24 Apr 1997 19:46:05 +0200
changeset 3047 599cb28f8502
parent 3046 6b7935317538
child 3048 a4b609108712
open General (type option is in Option in the newer versions, but always the top-level);
src/Pure/basis.ML
--- a/src/Pure/basis.ML	Thu Apr 24 19:41:00 1997 +0200
+++ b/src/Pure/basis.ML	Thu Apr 24 19:46:05 1997 +0200
@@ -34,6 +34,8 @@
     | valOf NONE     = raise Option
   end;
 
+open General;
+
 
 structure Int =
   struct