src/Pure/ROOT.ML
changeset 50255 d0ec1f0d1d7d
parent 50217 ce1f0602f48e
child 50450 358b6020f8b6
     1.1 --- a/src/Pure/ROOT.ML	Wed Nov 28 16:09:05 2012 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Nov 28 17:18:53 2012 +0100
     1.3 @@ -70,6 +70,10 @@
     1.4  
     1.5  (* concurrency within the ML runtime *)
     1.6  
     1.7 +if ML_System.name = "polyml-5.5.0"
     1.8 +then use "ML/ml_statistics_polyml-5.5.0.ML"
     1.9 +else use "ML/ml_statistics_dummy.ML";
    1.10 +
    1.11  use "Concurrent/single_assignment.ML";
    1.12  if Multithreading.available then ()
    1.13  else use "Concurrent/single_assignment_sequential.ML";