src/Pure/General/path.ML

   let val s = implode_path path
   in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
 
 val print = Pretty.unformatted_string_of o pretty;
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
 
 
 (* base element *)
 
 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s)