# HG changeset patch
# User wenzelm
# Date 1204836809 -3600
# Node ID 116d3cfc0d8933fc653e1961ae83e9aae17099af
# Parent  b8bbbb76220c621a71917fecbefea02e874f0cbc
replaced execute by system_out;

diff -r b8bbbb76220c -r 116d3cfc0d89 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Thu Mar 06 21:32:27 2008 +0100
+++ b/src/HOL/ex/svc_funcs.ML	Thu Mar 06 21:53:29 2008 +0100
@@ -64,10 +64,10 @@
       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;
-               execute (check_valid ^ " -dump-result " ^
+               #1 (system_out (check_valid ^ " -dump-result " ^
                         File.shell_path svc_output_file ^
                         " " ^ File.shell_path svc_input_file ^
-                        ">/dev/null 2>&1"))
+                        ">/dev/null 2>&1")))
       val svc_output =
         (case try File.read svc_output_file of
           SOME out => out