--- a/Nominal/Ex/Lambda.thy	Tue May 11 17:16:57 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 11 18:20:25 2010 +0200
@@ -15,7 +15,6 @@
 
 declare lam.perm[eqvt]
 
-declare permute_lam_raw.simps[eqvt]
 equivariance alpha_lam_raw
 
 section {* Strong Induction Principles*}
@@ -259,7 +258,6 @@
 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
 
-declare permute_lam_raw.simps[eqvt]
 equivariance alpha_lam_raw'
 
 thm eqvts_raw