diff -r 1909be313353 -r 1850361efb8f Nominal/Term5n.thy
--- a/Nominal/Term5n.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Term5n.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -169,7 +169,6 @@
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
-apply (metis flip_at_simps(1) supp_at_base supp_eqvt)
 done
 
 lemma lets_ok3:
@@ -186,7 +185,6 @@
 apply (simp add: alpha5_INJ alpha_gen)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)
-apply auto
 done
 
 lemma distinct_helper: