src/Pure/ROOT.ML
changeset 62501 98fa1f9a292f
parent 62498 5dfcc9697f29
child 62508 d0b68218ea55
     1.1 --- a/src/Pure/ROOT.ML	Wed Mar 02 19:43:31 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 03 11:12:02 2016 +0100
     1.3 @@ -101,9 +101,7 @@
     1.4  
     1.5  use "ML/exn_properties.ML";
     1.6  
     1.7 -if ML_System.name = "polyml-5.6"
     1.8 -then use "ML/ml_statistics.ML"
     1.9 -else use "ML/ml_statistics_dummy.ML";
    1.10 +use "ML/ml_statistics.ML";
    1.11  
    1.12  use "Concurrent/standard_thread.ML";
    1.13  use "Concurrent/single_assignment.ML";