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