src/Pure/ROOT.ML
changeset 62459 7a5d88dd8cc9
parent 62359 6709e51d5c11
child 62490 39d01eaf5292
     1.1 --- a/src/Pure/ROOT.ML	Sun Feb 28 19:56:57 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Sun Feb 28 21:20:51 2016 +0100
     1.3 @@ -96,11 +96,8 @@
     1.4  
     1.5  use "ML/exn_properties.ML";
     1.6  
     1.7 -if ML_System.name = "polyml-5.5.0"
     1.8 -  orelse ML_System.name = "polyml-5.5.1"
     1.9 -  orelse ML_System.name = "polyml-5.5.2"
    1.10 -  orelse ML_System.name = "polyml-5.6"
    1.11 -then use "ML/ml_statistics_polyml-5.5.0.ML"
    1.12 +if ML_System.name = "polyml-5.6"
    1.13 +then use "ML/ml_statistics.ML"
    1.14  else use "ML/ml_statistics_dummy.ML";
    1.15  
    1.16  use "Concurrent/standard_thread.ML";