src/Pure/General/ROOT.ML
changeset 28026 dad9a2f178ac
parent 28018 d3c5ab88fdcd
child 28128 565be25eb38f
--- 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";