src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Wed Apr 03 21:30:32 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 03 21:48:43 2013 +0200
@@ -28,9 +28,9 @@
 
 use "General/properties.ML";
 use "General/output.ML";
-use "General/timing.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";