# HG changeset patch
# User wenzelm
# Date 1204834051 -3600
# Node ID 3bfc71022dea350a23ead6e383b3ef3d261914fe
# Parent  5b4e5af10de6d451fcf4bb973bd6c520b77a8ebf
replaced execute by system_out;

diff -r 5b4e5af10de6 -r 3bfc71022dea src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Mar 06 20:46:41 2008 +0100
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Mar 06 21:07:31 2008 +0100
@@ -41,7 +41,7 @@
       val pmu =
         if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
         else eindhoven_home ^ "/pmu";
-    in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
+    in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
 in
   fn thy => fn goal =>
     let
diff -r 5b4e5af10de6 -r 3bfc71022dea src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Mar 06 20:46:41 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Mar 06 21:07:31 2008 +0100
@@ -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.shell_path mucke_input_file);
+    val (result, _) = system_out (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
   in
     if not (!trace_mc) then (File.rm mucke_input_file) else (); 
     result