use "xml.ML";
authorwenzelm
Sat, 08 Dec 2001 14:42:22 +0100
changeset 12420a2a05c952b4d
parent 12419 6a7ee57447aa
child 12421 54c06c1f88b8
use "xml.ML";
src/Pure/General/ROOT.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Sat Dec 08 14:42:03 2001 +0100
     1.2 +++ b/src/Pure/General/ROOT.ML	Sat Dec 08 14:42:22 2001 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4  use "buffer.ML";
     1.5  use "history.ML";
     1.6  use "pretty.ML";
     1.7 +use "xml.ML";
     1.8  
     1.9  structure PureGeneral =
    1.10  struct
    1.11 @@ -38,4 +39,5 @@
    1.12    structure Buffer = Buffer;
    1.13    structure History = History;
    1.14    structure Pretty = Pretty;
    1.15 +  structure XML = XML;
    1.16  end;