diff -r 6a7ee57447aa -r a2a05c952b4d src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Sat Dec 08 14:42:03 2001 +0100
+++ b/src/Pure/General/ROOT.ML	Sat Dec 08 14:42:22 2001 +0100
@@ -20,6 +20,7 @@
 use "buffer.ML";
 use "history.ML";
 use "pretty.ML";
+use "xml.ML";
 
 structure PureGeneral =
 struct
@@ -38,4 +39,5 @@
   structure Buffer = Buffer;
   structure History = History;
   structure Pretty = Pretty;
+  structure XML = XML;
 end;