changeset 37146 | f652333bbf8e |
parent 35010 | d6e492cea6e4 |
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Thu May 27 17:41:27 2010 +0200 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy Thu May 27 18:10:37 2010 +0200 @@ -32,7 +32,7 @@ oracle mc_eindhoven_oracle = {* let - val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global; + val eindhoven_term = Print_Mode.setmp ["Eindhoven"] o Syntax.string_of_term_global; fun call_mc s = let