src/HOL/Tools/SMT/smt_solver.ML
changeset 70293 c7e9d3a0a681
parent 70288 2e101846ad8f
child 70327 c04d4951a155
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon May 27 14:25:00 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon May 27 15:08:51 2019 +0200
@@ -49,7 +49,8 @@
 local
 
 fun make_command command options problem_path proof_path =
-  Bash.strings (command () @ options) ^ " " ^ File.bash_path problem_path ^
+  Bash.strings (command () @ options) ^ " " ^
+    Bash.string (File.platform_path problem_path) ^
     " > " ^ File.bash_path proof_path ^ " 2>&1"
 
 fun with_trace ctxt msg f x =