src/Pure/ROOT.ML
changeset 56287 ca090ae5f258
parent 56281 03c3d1a7c3b8
child 56288 bf1bdf335ea0
     1.1 --- a/src/Pure/ROOT.ML	Wed Mar 26 09:07:31 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Mar 26 09:13:38 2014 +0100
     1.3 @@ -26,11 +26,9 @@
     1.4  use "General/output.ML";
     1.5  use "PIDE/markup.ML";
     1.6  fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
     1.7 -use "General/timing.ML";
     1.8  use "General/scan.ML";
     1.9  use "General/source.ML";
    1.10  use "General/symbol.ML";
    1.11 -use "General/seq.ML";
    1.12  use "General/position.ML";
    1.13  use "General/symbol_pos.ML";
    1.14  use "General/antiquote.ML";
    1.15 @@ -54,6 +52,8 @@
    1.16  use "General/long_name.ML";
    1.17  use "General/binding.ML";
    1.18  use "General/socket_io.ML";
    1.19 +use "General/seq.ML";
    1.20 +use "General/timing.ML";
    1.21  
    1.22  use "General/sha1.ML";
    1.23  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();