diff -r 8857237c3a90 -r 19afb533028e src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 03 11:59:03 2016 +0100
@@ -65,7 +65,7 @@
           let
             val xml =
               ML_Name_Space.displayTypeExpression (types, depth, space)
-              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+              |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of
               |> Output.output |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;
@@ -193,7 +193,7 @@
         val pos = Exn_Properties.position_of loc;
         val txt =
           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
-          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
+          Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
       in if hard then err txt else warn txt end;
 
 
@@ -205,7 +205,8 @@
       let
         fun display disp x =
           if depth > 0 then
-            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
+            (write (disp x |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of);
+              write "\n")
           else ();
 
         fun apply_fix (a, b) =