--- 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