--- a/src/Pure/General/path.ML Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/General/path.ML Fri Mar 18 16:26:35 2016 +0100
@@ -173,6 +173,8 @@
val print = Pretty.unformatted_string_of o pretty;
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+
(* base element *)