diff -r 66d388a84e3c -r 50838e25f73c Nominal/TySch.thy --- a/Nominal/TySch.thy Fri Mar 19 15:43:43 2010 +0100 +++ b/Nominal/TySch.thy Fri Mar 19 15:43:59 2010 +0100 @@ -7,8 +7,6 @@ ML {* val _ = cheat_fv_rsp := false *} ML {* val _ = cheat_const_rsp := false *} ML {* val _ = cheat_equivp := false *} -ML {* val _ = cheat_fv_eqvt := false *} -ML {* val _ = cheat_alpha_eqvt := false *} nominal_datatype t = Var "name"