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