exported File.shell_quote;

--- 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 <> ""

--- 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