diff -r 7ede6ca96c61 -r ca090ae5f258 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Mar 26 09:07:31 2014 +0100
+++ b/src/Pure/ROOT.ML	Wed Mar 26 09:13:38 2014 +0100
@@ -26,11 +26,9 @@
 use "General/output.ML";
 use "PIDE/markup.ML";
 fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
-use "General/timing.ML";
 use "General/scan.ML";
 use "General/source.ML";
 use "General/symbol.ML";
-use "General/seq.ML";
 use "General/position.ML";
 use "General/symbol_pos.ML";
 use "General/antiquote.ML";
@@ -54,6 +52,8 @@
 use "General/long_name.ML";
 use "General/binding.ML";
 use "General/socket_io.ML";
+use "General/seq.ML";
+use "General/timing.ML";
 
 use "General/sha1.ML";
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();