src/Pure/ROOT.ML
changeset 38266 492d377ecfe2
parent 38150 67fc24df3721
child 38271 36187e8443dd
--- 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";