src/Pure/PIDE/xml.ML
changeset 62819 d3ff367a16a0
parent 62663 bea354f6ff21
child 63806 c54a53ef1873
--- a/src/Pure/PIDE/xml.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/PIDE/xml.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -170,8 +170,7 @@
 fun pretty depth tree =
   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
 
-val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));