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