--- a/src/Pure/General/ROOT.ML Wed Aug 27 20:36:23 2008 +0200+++ b/src/Pure/General/ROOT.ML Wed Aug 27 20:36:25 2008 +0200@@ -30,8 +30,8 @@ use "susp.ML"; use "path.ML"; use "url.ML";+use "buffer.ML"; use "file.ML";-use "buffer.ML"; use "xml.ML"; use "yxml.ML";