diff -r 892fcdb96c96 -r aeed597d2043 Nominal/Parser.thy --- a/Nominal/Parser.thy Tue Mar 23 08:22:48 2010 +0100 +++ b/Nominal/Parser.thy Tue Mar 23 08:33:48 2010 +0100 @@ -265,7 +265,8 @@ end *} -ML {* val cheat_equivp = Unsynchronized.ref true *} +(* This one is not needed for the proper examples *) +ML {* val cheat_equivp = Unsynchronized.ref false *} (* These 4 are not needed any more *) ML {* val cheat_fv_rsp = Unsynchronized.ref false *}