src/Pure/ML-Systems/polyml-5.5.2.ML
2013-12-12 ago added missing file (cf. 124432e77ecf);