changeset 1595 | aeed597d2043 |
parent 1581 | 6b1eea8dcdc0 |
child 1615 | 0ea578c6dae3 |
--- 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 *}