diff -r 374e2f90140c -r d629240f0f63 Nominal/Ex/LetRec.thy
--- a/Nominal/Ex/LetRec.thy	Sun Jul 17 11:33:09 2011 +0100
+++ b/Nominal/Ex/LetRec.thy	Mon Jul 18 00:21:51 2011 +0100
@@ -27,8 +27,6 @@
 thm let_rec.fv_bn_eqvt
 thm let_rec.size_eqvt
 
-lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
-  by (simp add: permute_pure)
 
 nominal_primrec
     height_trm :: "trm \<Rightarrow> nat"
@@ -56,8 +54,9 @@
   apply (rule trans)
   apply(rule_tac p="p" in supp_perm_eq[symmetric])
   apply (simp add: pure_supp fresh_star_def)
-  apply (simp only: eqvts)
-  apply (simp add: eqvt_at_def)
+  apply(simp add: eqvt_at_def)
+  apply(perm_simp)
+  apply (simp add: permute_fun_def)
   done
 
 termination by lexicographic_order