diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -116,7 +116,7 @@
 
 local
   fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
-  fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
+  fun pretty_value depth = "ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))";
 in
 
 fun make_string_fn local_env =