diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Mon May 10 15:45:04 2010 +0200
@@ -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*}
 
 (*