proper platform_path for Windows;

--- a/src/HOL/Library/code_test.ML	Thu Sep 24 17:23:25 2020 +0200
+++ b/src/HOL/Library/code_test.ML	Thu Sep 24 19:04:47 2020 +0200
@@ -311,7 +311,7 @@
       string start_markerN ^
       \<^verbatim>\<open> ^ String.concat (map format result) ^ \<close> ^
       string end_markerN ^ \<^verbatim>\<open>
-    val out = BinIO.openOut \<close> ^ string (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>
+    val out = BinIO.openOut \<close> ^ ML_Syntax.print_platform_path out_path ^ \<^verbatim>\<open>
     val _ = BinIO.output (out, Byte.stringToBytes result_text)
     val _ = BinIO.closeOut out
   in () end;

--- 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 =