src/Pure/ROOT.ML
changeset 43729 07d3c6afa865
parent 43712 3c2c912af2ef
child 43746 a41f618c641d
--- a/src/Pure/ROOT.ML	Sun Jul 10 16:31:04 2011 +0200
+++ b/src/Pure/ROOT.ML	Sun Jul 10 16:34:17 2011 +0200
@@ -127,6 +127,7 @@
 
 use "term_ord.ML";
 use "term_subst.ML";
+use "term_xml.ML";
 use "old_term.ML";
 use "General/name_space.ML";
 use "sorts.ML";