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