diff -r 90c88e7ef62d -r 3ff9cfc5c403 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Fri Apr 16 18:30:51 2004 +0200
+++ b/src/Pure/General/ROOT.ML	Fri Apr 16 18:40:21 2004 +0200
@@ -5,6 +5,9 @@
 *)
 
 use "table.ML";
+use "scan.ML";
+use "source.ML";
+use "symbol.ML";
 use "graph.ML";
 use "heap.ML";
 use "object.ML";
@@ -14,9 +17,6 @@
 use "lazy_scan.ML";
 use "name_space.ML";
 use "position.ML";
-use "scan.ML";
-use "source.ML";
-use "symbol.ML";
 use "path.ML";
 use "url.ML";
 use "file.ML";