diff -r 697e5688f370 -r 03628da91b07 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Thu Sep 24 17:23:25 2020 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Thu Sep 24 19:04:47 2020 +0200
@@ -20,6 +20,7 @@
   val print_string: string -> string
   val print_strings: string list -> string
   val print_path: Path.T -> string
+  val print_platform_path: Path.T -> string
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
   val print_range: Position.range -> string
@@ -91,6 +92,8 @@
 fun print_path path =
   "Path.explode " ^ print_string (Path.implode path);
 
+val print_platform_path = print_string o File.platform_path;
+
 val print_properties = print_list (print_pair print_string print_string);
 
 fun print_position pos =