diff -r dfea9e739231 -r b93b631570ca Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Thu Feb 04 15:19:24 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Thu Feb 04 17:39:04 2010 +0100
@@ -29,7 +29,7 @@
 apply(auto)
 apply(drule_tac x="p \<bullet> xa" in bspec)
 apply(unfold mem_def permute_fun_def)[1] 
-apply(simp add: eqvts)
+apply(simp add: eqvts del: permute_eqvt)
 apply(simp add: fresh_permute_iff)
 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
 apply(simp)