diff -r 06c87d2c5b5a -r edf497b5b5d2 src/Pure/ML-Systems/install_pp_polyml-5.3.ML --- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Mon Nov 09 20:47:39 2009 +0100 +++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Mon Nov 09 21:30:54 2009 +0100 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML -Extra toplevel pretty-printing for Poly/ML 5.3. +Extra toplevel pretty-printing for Poly/ML 5.3.0. *) PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>