src/Pure/ROOT.ML
changeset 51606 2843cc095a57
parent 51551 88d1d19fb74f
child 51933 a60c6c90a447
     1.1 --- a/src/Pure/ROOT.ML	Wed Apr 03 21:30:32 2013 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Apr 03 21:48:43 2013 +0200
     1.3 @@ -28,9 +28,9 @@
     1.4  
     1.5  use "General/properties.ML";
     1.6  use "General/output.ML";
     1.7 -use "General/timing.ML";
     1.8  use "PIDE/markup.ML";
     1.9  fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
    1.10 +use "General/timing.ML";
    1.11  use "General/scan.ML";
    1.12  use "General/source.ML";
    1.13  use "General/symbol.ML";