1.1 --- a/src/Pure/ROOT.ML Sat Jun 25 15:08:58 2011 +0200
1.2 +++ b/src/Pure/ROOT.ML Sat Jun 25 17:17:49 2011 +0200
1.3 @@ -44,8 +44,6 @@
1.4 use "General/balanced_tree.ML";
1.5 use "General/graph.ML";
1.6 use "General/linear_set.ML";
1.7 -use "General/long_name.ML";
1.8 -use "General/binding.ML";
1.9 use "General/path.ML";
1.10 use "General/url.ML";
1.11 use "General/buffer.ML";
1.12 @@ -54,6 +52,8 @@
1.13 use "General/xml_data.ML";
1.14 use "General/yxml.ML";
1.15 use "General/pretty.ML";
1.16 +use "General/long_name.ML";
1.17 +use "General/binding.ML";
1.18
1.19 use "General/sha1.ML";
1.20 if String.isPrefix "polyml" ml_system