tuned load order;
authorwenzelm
Wed, 26 Mar 2014 09:13:38 +0100
changeset 56287 ca090ae5f258
parent 56286 7ede6ca96c61
child 56288 bf1bdf335ea0
tuned load order;
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 ();