src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/ROOT.ML	Wed Nov 28 17:18:53 2012 +0100
@@ -70,6 +70,10 @@
 
 (* concurrency within the ML runtime *)
 
+if ML_System.name = "polyml-5.5.0"
+then use "ML/ml_statistics_polyml-5.5.0.ML"
+else use "ML/ml_statistics_dummy.ML";
+
 use "Concurrent/single_assignment.ML";
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";