src/Pure/ROOT.ML
changeset 43746 a41f618c641d
parent 43729 07d3c6afa865
child 43748 c70bd78ec83c
     1.1 --- a/src/Pure/ROOT.ML	Mon Jul 11 10:27:50 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Jul 11 11:13:33 2011 +0200
     1.3 @@ -27,9 +27,9 @@
     1.4  if Multithreading.available then ()
     1.5  else use "Concurrent/synchronized_sequential.ML";
     1.6  
     1.7 +use "General/properties.ML";
     1.8  use "General/output.ML";
     1.9  use "General/timing.ML";
    1.10 -use "General/properties.ML";
    1.11  use "General/markup.ML";
    1.12  use "General/scan.ML";
    1.13  use "General/source.ML";