src/HOL/Library/Old_SMT/old_smt_solver.ML
changeset 62549 9498623b27f0
parent 61268 abe08fb15a12
child 64304 96bc94c87a81
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Mon Mar 07 20:44:47 2016 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Mon Mar 07 21:09:28 2016 +0100
@@ -51,9 +51,10 @@
 
 local
 
-fun make_cmd command options problem_path proof_path = space_implode " " (
-  "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
-  [File.shell_path problem_path, ")", ">", File.shell_path proof_path])
+fun make_cmd command options problem_path proof_path =
+  space_implode " "
+    ("(exec 2>&1;" :: map File.bash_string (command () @ options) @
+      [File.bash_path problem_path, ")", ">", File.bash_path proof_path])
 
 fun trace_and ctxt msg f x =
   let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) ()
@@ -82,7 +83,7 @@
             Cache_IO.run_and_cache certs key mk_cmd input
       | (SOME output, _) =>
           trace_and ctxt ("Using cached certificate from " ^
-            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
+            Path.print (Cache_IO.cache_path_of certs) ^ " ...")
             I output))
 
 fun run_solver ctxt name mk_cmd input =