diff -r 6b7935317538 -r 599cb28f8502 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