# HG changeset patch
# User wenzelm
# Date 861903965 -7200
# Node ID 599cb28f8502e23d570bc13e9560bdad71017595
# Parent  6b7935317538c8f4c42aaa202a71838e5037874e
open General (type option is in Option in the newer versions, but always
  the top-level);

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