--- a/src/Pure/General/ROOT.ML Wed Jan 13 12:16:34 1999 +0100
+++ b/src/Pure/General/ROOT.ML Wed Jan 13 12:44:33 1999 +0100
@@ -12,6 +12,10 @@
use "path.ML";
use "file.ML";
use "history.ML";
+use "scan.ML";
+use "source.ML";
+use "symbol.ML";
+use "pretty.ML";
structure PureGeneral =
struct
@@ -23,4 +27,8 @@
structure Path = Path;
structure File = File;
structure History = History;
+ structure Scan = Scan;
+ structure Source = Source;
+ structure Symbol = Symbol;
+ structure Pretty = Pretty;
end;