# HG changeset patch
# User wenzelm
# Date 1672756374 -3600
# Node ID d9913b41a7bc52772ca60d20f4f6d3b029f07eec
# Parent  b59118d11a4615784d2dd698e88a622681d4c2ad
tuned;

diff -r b59118d11a46 -r d9913b41a7bc src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Tue Jan 03 15:03:48 2023 +0100
+++ b/src/HOL/Library/code_test.ML	Tue Jan 03 15:32:54 2023 +0100
@@ -503,7 +503,7 @@
         case (false, Some(t)) => "False" + t(()) + "\n"
       }).mkString
   isabelle.File.write(
-    isabelle.Path.explode(\<close> ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>),
+    isabelle.Path.explode(\<close> ^ quote (File.standard_path out_path) ^ \<^verbatim>\<open>),
     \<close> ^ quote start_marker ^ \<^verbatim>\<open> + result_text + \<close> ^ quote end_marker ^ \<^verbatim>\<open>)
 }\<close>
     val _ = File.write code_path code
diff -r b59118d11a46 -r d9913b41a7bc src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 03 15:03:48 2023 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Tue Jan 03 15:32:54 2023 +0100
@@ -1136,7 +1136,7 @@
 
 exception Execute of string;
 
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
+fun tmp_file s = File.standard_path (File.tmp_path (Path.basic s));
 fun wrap s = "\""^s^"\"";
 
 fun solve_glpk prog =