--- a/Nominal/Ex/Lambda.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/Lambda.thy	Sun May 09 12:26:10 2010 +0100
@@ -15,6 +15,10 @@
 
 declare lam.perm[eqvt]
 
+declare permute_lam_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_lam_raw
+
 section {* Strong Induction Principles*}
 
 (*