1.1 --- a/src/Pure/ROOT.ML	Wed Sep 18 13:18:51 2013 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Sep 18 13:31:44 2013 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4  then use "ML/exn_trace_polyml-5.5.1.ML"
     1.5  else ();
     1.6  
     1.7 -if ML_System.name = "polyml-5.5.0"
     1.8 +if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1"
     1.9  then use "ML/ml_statistics_polyml-5.5.0.ML"
    1.10  else use "ML/ml_statistics_dummy.ML";
    1.11