# HG changeset patch
# User wenzelm
# Date 1087828749 -7200
# Node ID ff1c919f49829e324e294b81ea8dde87ccf76c79
# Parent  e73f8140af783c2f89e79470d5762f826d2be8d9
File.quote_sysify_path;

diff -r e73f8140af78 -r ff1c919f4982 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 21 10:25:57 2004 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 21 16:39:09 2004 +0200
@@ -500,7 +500,7 @@
       else mucke_home ^ "/mucke";
     val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
     val _ = File.write mucke_input_file s;
-    val result = execute (mucke ^ " -nb -res " ^ (File.sysify_path mucke_input_file));
+    val result = execute (mucke ^ " -nb -res " ^ (File.quote_sysify_path mucke_input_file));
   in
     if not (!trace_mc) then (File.rm mucke_input_file) else (); 
     result
diff -r e73f8140af78 -r ff1c919f4982 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Mon Jun 21 10:25:57 2004 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Mon Jun 21 16:39:09 2004 +0200
@@ -71,9 +71,9 @@
       val svc_output_file = File.tmp_path (Path.basic "SVM_out");
       val _ = (File.write svc_input_file svc_input;
 	       execute (check_valid ^ " -dump-result " ^ 
-			File.sysify_path svc_output_file ^
-			" " ^ File.sysify_path svc_input_file ^ 
-			"> /dev/null 2>&1"))
+			File.quote_sysify_path svc_output_file ^
+			" " ^ File.quote_sysify_path svc_input_file ^ 
+			">/dev/null 2>&1"))
       val svc_output =
         (case Library.try File.read svc_output_file of
           Some out => out