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