| changeset 24634 | 38db11874724 |
| parent 22819 | a7b425bb668c |
| child 26225 | 3bfc71022dea |
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 18 18:05:34 2007 +0200 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 18 18:05:37 2007 +0200 @@ -33,8 +33,7 @@ oracle mc_eindhoven_oracle ("term") = {* let - val eindhoven_term = - setmp print_mode ["Eindhoven"] o Sign.string_of_term; + val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Sign.string_of_term; fun call_mc s = let