diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Ex/LetRec.thy
--- a/Nominal/Ex/LetRec.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/LetRec.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -46,8 +46,10 @@
   apply (case_tac b rule: let_rec.exhaust(2))
   apply blast
   apply (erule Abs_set_fcb)
-  apply (simp_all add: pure_fresh)
-  apply (simp add: eqvt_at_def)
+  apply (simp_all add: pure_fresh)[2]
+  apply (simp only: eqvt_at_def)
+  apply(perm_simp)
+  apply(simp)
   apply (simp add: Abs_eq_iff2)
   apply (simp add: alphas)
   apply clarify
@@ -55,8 +57,6 @@
   apply(rule_tac p="p" in supp_perm_eq[symmetric])
   apply (simp add: pure_supp fresh_star_def)
   apply(simp add: eqvt_at_def)
-  apply(perm_simp)
-  apply (simp add: permute_fun_def)
   done
 
 termination (eqvt) by lexicographic_order