| changeset 61794 | 4c232a2ddeab |
| parent 61715 | 5dc95d957569 |
| child 62354 | fdd6989cc8a0 |
--- a/src/Pure/ROOT.ML Sun Dec 06 17:27:42 2015 +0100 +++ b/src/Pure/ROOT.ML Sun Dec 06 23:10:08 2015 +0100 @@ -105,7 +105,6 @@ if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1" orelse ML_System.name = "polyml-5.5.2" - orelse ML_System.name = "polyml-5.5.3" orelse ML_System.name = "polyml-5.6" then use "ML/ml_statistics_polyml-5.5.0.ML" else use "ML/ml_statistics_dummy.ML";