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