| changeset 54723 | 124432e77ecf |
| parent 54718 | 8c5221d698cd |
| child 56275 | 600f432ab556 |
--- a/src/Pure/ML-Systems/polyml.ML Thu Dec 12 13:23:23 2013 +0100 +++ b/src/Pure/ML-Systems/polyml.ML Thu Dec 12 13:50:44 2013 +0100 @@ -44,9 +44,6 @@ else use "ML-Systems/single_assignment_polyml.ML"; open Thread; -if ML_System.name = "polyml-5.5.2" then () -else use "ML-Systems/thread_physical_processors.ML"; - use "ML-Systems/multithreading.ML"; use "ML-Systems/multithreading_polyml.ML";