--- a/src/Pure/ROOT.ML Tue Aug 10 20:13:52 2010 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 10 22:26:23 2010 +0200
@@ -50,6 +50,7 @@
use "General/buffer.ML";
use "General/file.ML";
use "General/xml.ML";
+use "General/xml_data.ML";
use "General/yxml.ML";
use "General/sha1.ML";