# HG changeset patch
# User wenzelm
# Date 1255614350 -7200
# Node ID 2cb928848e77a73ff3e34313b9b57b0c67a1b978
# Parent  b6711ec9de26e9a40b860a8c871140680c72ecda
exported File.shell_quote;

diff -r b6711ec9de26 -r 2cb928848e77 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 <> ""
diff -r b6711ec9de26 -r 2cb928848e77 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Oct 15 12:23:24 2009 +0200
+++ b/src/Pure/General/file.ML	Thu Oct 15 15:45:50 2009 +0200
@@ -7,6 +7,7 @@
 signature FILE =
 sig
   val platform_path: Path.T -> string
+  val shell_quote: string -> string
   val shell_path: Path.T -> string
   val cd: Path.T -> unit
   val pwd: unit -> Path.T