changeset 35010 | d6e492cea6e4 |
parent 32740 | 9dd0a2f83429 |
child 37146 | f652333bbf8e |
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Sat Feb 06 14:39:33 2010 +0100 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy Sat Feb 06 14:50:55 2010 +0100 @@ -40,7 +40,7 @@ val pmu = if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set" else eindhoven_home ^ "/pmu"; - in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end; + in #1 (bash_output ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end; in fn cgoal => let