--- a/Nominal/Ex/TypeSchemes.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Sun May 09 12:26:10 2010 +0100
@@ -14,6 +14,11 @@
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
 
+declare permute_ty_raw_permute_tys_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_ty_raw
+
+
 (* below we define manually the function for size *)
 
 lemma size_eqvt_raw: