diff -r 3201a8c3456b -r 9b109ef7bf47 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed May 12 16:32:44 2010 +0200 +++ b/Nominal/NewParser.thy Wed May 12 16:39:10 2010 +0200 @@ -275,7 +275,6 @@ end *} -ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} ML {* val cheat_equivp = Unsynchronized.ref false *} ML {* val cheat_fv_rsp = Unsynchronized.ref false *} ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}