src/Pure/ML-Systems/compiler_polyml.ML
2013-01-16 ago tuned comments;
2012-05-24 ago simplified Poly/ML setup -- 5.3.0 is now the common base-line;