--- a/src/HOL/Library/code_test.ML Sat Oct 07 20:31:01 2017 +0200
+++ b/src/HOL/Library/code_test.ML Sun Oct 08 12:42:20 2017 +0200
@@ -425,8 +425,8 @@
"end;"
val ml_source =
"Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
- "use " ^ ML_Syntax.print_string (Path.implode (Path.expand code_path)) ^
- "; use " ^ ML_Syntax.print_string (Path.implode (Path.expand driver_path)) ^
+ "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^
+ "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^
"; Test.main ();"
val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\""
in