--- a/Nominal/Ex/Let.thy	Sun Jul 17 11:33:09 2011 +0100
+++ b/Nominal/Ex/Let.thy	Mon Jul 18 00:21:51 2011 +0100
@@ -79,9 +79,6 @@
 done
 
 
-lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
-  by (simp add: permute_pure)
-
 function
   apply_assn :: "(trm \<Rightarrow> nat) \<Rightarrow> assn \<Rightarrow> nat"
 where