src/Pure/General/ROOT.ML
changeset 6116 8ba2f25610f7
parent 5864 30b6a3251813
child 6134 ec6092b0599d
--- 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;