diff -r 2733b240bfea -r d3ff367a16a0 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/morphism.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -71,7 +71,7 @@
 
 fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
 fun binding (Morphism {binding, ...}) = apply binding;
 fun typ (Morphism {typ, ...}) = apply typ;