src/Pure/ROOT.ML
changeset 43767 e0219ef7f84c
parent 43748 c70bd78ec83c
child 43776 6dd13e111d30
--- a/src/Pure/ROOT.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/ROOT.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -53,7 +53,6 @@
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/xml.ML";
-use "General/xml_data.ML";
 use "General/pretty.ML";
 use "General/path.ML";
 use "General/url.ML";