--- a/src/HOL/ex/svc_funcs.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/HOL/ex/svc_funcs.ML Sat Feb 06 14:50:55 2010 +0100
@@ -62,11 +62,11 @@
val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
val svc_input_file = File.tmp_path (Path.basic "SVM_in");
val svc_output_file = File.tmp_path (Path.basic "SVM_out");
- val _ = (File.write svc_input_file svc_input;
- #1 (system_out (check_valid ^ " -dump-result " ^
- File.shell_path svc_output_file ^
- " " ^ File.shell_path svc_input_file ^
- ">/dev/null 2>&1")))
+ val _ = File.write svc_input_file svc_input;
+ val _ =
+ bash_output (check_valid ^ " -dump-result " ^
+ File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
+ ">/dev/null 2>&1")
val svc_output =
(case try File.read svc_output_file of
SOME out => out