src/Pure/ML/ml_syntax.ML

   val print_symbol_char: Symbol.symbol -> string
   val print_symbol: Symbol.symbol -> string
   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
   val print_path_binding: Path.binding -> string
   val make_binding: string * Position.T -> string

 val print_strings = print_list print_string;
 
 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 =
   "Position.of_properties " ^ print_properties (Position.properties_of pos);