--- a/Nominal/Nominal2_Abs.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -249,7 +249,7 @@
   unfolding Diff_eqvt[symmetric]
   apply(erule_tac [!] exE)
   apply(rule_tac [!] x="p \<bullet> pa" in exI)
-  by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
+  by (auto simp only: fresh_star_permute_iff permute_eqvt[symmetric])
 
 
 section {* Strengthening the equivalence *}