src/Pure/General/ROOT.ML
changeset 6317 128e592f5489
parent 6222 2b24cf477313
child 6634 6f74e7aa5b4d
--- a/src/Pure/General/ROOT.ML	Tue Mar 09 12:08:50 1999 +0100
+++ b/src/Pure/General/ROOT.ML	Tue Mar 09 12:09:05 1999 +0100
@@ -12,6 +12,7 @@
 use "position.ML";
 use "path.ML";
 use "file.ML";
+use "buffer.ML";
 use "history.ML";
 use "scan.ML";
 use "source.ML";
@@ -28,6 +29,7 @@
   structure Position = Position;
   structure Path = Path;
   structure File = File;
+  structure Buffer = Buffer;
   structure History = History;
   structure Scan = Scan;
   structure Source = Source;