src/Pure/General/ROOT.ML
changeset 5864 30b6a3251813
parent 5040 78abd4c4802a
child 6116 8ba2f25610f7
equal deleted inserted replaced
5863:9935800edf58 5864:30b6a3251813
    10 use "name_space.ML";
    10 use "name_space.ML";
    11 use "position.ML";
    11 use "position.ML";
    12 use "path.ML";
    12 use "path.ML";
    13 use "file.ML";
    13 use "file.ML";
    14 use "history.ML";
    14 use "history.ML";
       
    15 
       
    16 structure PureGeneral =
       
    17 struct
       
    18   structure Symtab = Symtab;
       
    19   structure Object = Object;
       
    20   structure Seq = Seq;
       
    21   structure NameSpace = NameSpace;
       
    22   structure Position = Position;
       
    23   structure Path = Path;
       
    24   structure File = File;
       
    25   structure History = History;
       
    26 end;