--- 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 ();