src/Pure/General/ROOT.ML
changeset 6116 8ba2f25610f7
parent 5864 30b6a3251813
child 6134 ec6092b0599d
     1.1 --- a/src/Pure/General/ROOT.ML	Wed Jan 13 12:16:34 1999 +0100
     1.2 +++ b/src/Pure/General/ROOT.ML	Wed Jan 13 12:44:33 1999 +0100
     1.3 @@ -12,6 +12,10 @@
     1.4  use "path.ML";
     1.5  use "file.ML";
     1.6  use "history.ML";
     1.7 +use "scan.ML";
     1.8 +use "source.ML";
     1.9 +use "symbol.ML";
    1.10 +use "pretty.ML";
    1.11  
    1.12  structure PureGeneral =
    1.13  struct
    1.14 @@ -23,4 +27,8 @@
    1.15    structure Path = Path;
    1.16    structure File = File;
    1.17    structure History = History;
    1.18 +  structure Scan = Scan;
    1.19 +  structure Source = Source;
    1.20 +  structure Symbol = Symbol;
    1.21 +  structure Pretty = Pretty;
    1.22  end;