diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Let.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -75,7 +75,6 @@
 apply(simp add: trm_assn.perm_bn_simps)
 apply(simp add: trm_assn.perm_bn_simps)
 apply(simp add: trm_assn.bn_defs)
-apply(simp add: atom_eqvt)
 done
 
 
@@ -95,11 +94,10 @@
 lemma [eqvt]:
   "p \<bullet> (apply_assn f a) = apply_assn (p \<bullet> f) (p \<bullet> a)"
   apply(induct f a rule: apply_assn.induct)
-  apply simp_all
+  apply simp
+  apply(simp only: apply_assn.simps trm_assn.perm_simps)
   apply(perm_simp)
-  apply rule
-  apply(perm_simp)
-  apply simp
+  apply(simp)
   done
 
 lemma alpha_bn_apply_assn:
@@ -155,8 +153,6 @@
   "p \<bullet> (apply_assn2 f a) = apply_assn2 (p \<bullet> f) (p \<bullet> a)"
   apply(induct f a rule: apply_assn2.induct)
   apply simp_all
-  apply(perm_simp)
-  apply rule
   done
 
 lemma bn_apply_assn2: "bn (apply_assn2 f as) = bn as"