src/HOL/SMT/Tools/smt_solver.ML

--- a/src/HOL/SMT/Tools/smt_solver.ML	Thu Oct 15 12:23:24 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Thu Oct 15 15:45:50 2009 +0200
@@ -114,7 +114,7 @@
 
 fun run_solver ctxt {env_var, remote_name} args output =
   let
-    val qf = File.shell_path and qq = enclose "'" "'"
+    val qf = File.shell_path and qq = File.shell_quote
     val path = getenv env_var and remote = getenv "REMOTE_SMT_SOLVER"
     fun cmd f1 f2 =
       if path <> ""