diff -r 5408e5207131 -r d6e492cea6e4 src/HOL/ex/svc_funcs.ML
--- 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