diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -451,7 +451,7 @@
 (* toplevel pretty printing *)
 
 val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ =>
+  ML_system_pp (fn _ => fn _ =>
     Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
 
 end;