--- a/src/Pure/General/ROOT.ML Tue Aug 14 13:20:21 2007 +0200 +++ b/src/Pure/General/ROOT.ML Tue Aug 14 13:20:47 2007 +0200 @@ -27,3 +27,5 @@ use "file.ML"; use "buffer.ML"; use "history.ML"; +use "xml.ML"; +