src/Pure/ML/ml_syntax.ML

--- a/src/Pure/ML/ml_syntax.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -124,7 +124,7 @@
   in Pretty.str (quote (implode (map print_char body'))) end;
 
 val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
+  ML_system_pp (fn depth => fn _ => fn str =>
     Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
 
 end;