--- a/Nominal/Ex/Exec/Lambda_Exec.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/Ex/Exec/Lambda_Exec.thy	Thu May 24 10:17:32 2012 +0200
@@ -458,10 +458,6 @@
 value "(atom N0 \<rightleftharpoons> atom N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))"
 value "subst ((N0 \<leftrightarrow> N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))) N1 (Var N0)"*)
 
-lemma [eqvt]:
-  "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
-  unfolding Let_def permute_fun_app_eq ..
-
 end