--- a/Nominal/Nominal2_Base.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu May 24 10:17:32 2012 +0200
@@ -1093,6 +1093,9 @@
 unfolding finite_def
 by (perm_simp) (rule refl)
 
+lemma Let_eqvt [eqvt]:
+  "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
+  unfolding Let_def permute_fun_app_eq ..
 
 subsubsection {* Equivariance for product operations *}