diff -r 5f5608bfe230 -r 124432e77ecf src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Dec 12 13:23:23 2013 +0100
+++ b/src/Pure/ROOT	Thu Dec 12 13:50:44 2013 +0100
@@ -12,6 +12,7 @@
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml.ML"
+    "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
     "ML-Systems/single_assignment.ML"
@@ -19,7 +20,6 @@
     "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
-    "ML-Systems/thread_physical_processors.ML"
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
@@ -36,13 +36,13 @@
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
     "ML-Systems/polyml.ML"
+    "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
     "ML-Systems/single_assignment.ML"
     "ML-Systems/single_assignment_polyml.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
-    "ML-Systems/thread_physical_processors.ML"
     "ML-Systems/universal.ML"
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"