--- a/Quot/Nominal/LamEx.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -120,10 +120,11 @@
 apply(rule_tac x="pi \<bullet> pia" in exI)
 apply(rule conjI)
 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
+apply(simp only: Diff_eqvt rfv_eqvt insert_eqvt atom_eqvt empty_eqvt)
+apply(simp)
 apply(rule conjI)
 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
+apply(simp add: Diff_eqvt rfv_eqvt atom_eqvt insert_eqvt empty_eqvt)
 apply(subst permute_eqvt[symmetric])
 apply(simp)
 done
@@ -619,5 +620,5 @@
 
 
 
-end<
+end