--- a/src/HOL/Modelcheck/mucke_oracle.ML Sun Jun 05 11:31:20 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Sun Jun 05 11:31:21 2005 +0200
@@ -503,7 +503,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.quote_sysify_path mucke_input_file));
+ val result = execute (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
in
if not (!trace_mc) then (File.rm mucke_input_file) else ();
result
--- a/src/HOL/ex/svc_funcs.ML Sun Jun 05 11:31:20 2005 +0200
+++ b/src/HOL/ex/svc_funcs.ML Sun Jun 05 11:31:21 2005 +0200
@@ -71,8 +71,8 @@
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.quote_sysify_path svc_output_file ^
- " " ^ File.quote_sysify_path svc_input_file ^
+ File.shell_path svc_output_file ^
+ " " ^ File.shell_path svc_input_file ^
">/dev/null 2>&1"))
val svc_output =
(case Library.try File.read svc_output_file of
--- a/src/Pure/Isar/isar_cmd.ML Sun Jun 05 11:31:20 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Jun 05 11:31:21 2005 +0200
@@ -188,12 +188,12 @@
(* present draft files *)
fun display_drafts files = Toplevel.imperative (fn () =>
- let val outfile = File.quote_sysify_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
- in system ("\"$ISATOOL\" display -c " ^ outfile ^ " &"); () end);
+ let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
+ in File.isatool ("display -c " ^ outfile ^ " &"); () end);
fun print_drafts files = Toplevel.imperative (fn () =>
- let val outfile = File.quote_sysify_path (Present.drafts "ps" files)
- in system ("\"$ISATOOL\" print -c " ^ outfile); () end);
+ let val outfile = File.shell_path (Present.drafts "ps" files)
+ in File.isatool ("print -c " ^ outfile); () end);
(* pretty_setmargin *)