src/Pure/basis.ML
changeset 3047 599cb28f8502
parent 2884 4f2a4c27f9b5
child 3244 71b760618f30
--- 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