src/Pure/ROOT.ML
changeset 43547 f3a8476285c6
parent 42504 869c3f6f2d6e
child 43593 11140987d415
--- a/src/Pure/ROOT.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -44,8 +44,6 @@
 use "General/balanced_tree.ML";
 use "General/graph.ML";
 use "General/linear_set.ML";
-use "General/long_name.ML";
-use "General/binding.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/buffer.ML";
@@ -54,6 +52,8 @@
 use "General/xml_data.ML";
 use "General/yxml.ML";
 use "General/pretty.ML";
+use "General/long_name.ML";
+use "General/binding.ML";
 
 use "General/sha1.ML";
 if String.isPrefix "polyml" ml_system