--- a/Quot/Nominal/Terms.thy	Wed Feb 03 12:34:53 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:45:06 2010 +0100
@@ -104,16 +104,13 @@
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
-apply (simp_all add: eqvts)
-apply (rule atom_eqvt)
+apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
 done
 
 lemma rfv_trm1_eqvt[eqvt]:
   shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
   apply (induct t)
-  apply (simp_all add: eqvts)
-  apply (rule atom_eqvt) 
-  apply (simp add: atom_eqvt) 
+  apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
   done
 
 
@@ -127,10 +124,10 @@
   apply(erule conjE)+
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt eqvts)
+  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt rfv_trm1_eqvt)
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: eqvts atom_eqvt)
+  apply(simp add: atom_eqvt Diff_eqvt rfv_trm1_eqvt insert_eqvt empty_eqvt)
   apply(simp add: permute_eqvt[symmetric])
   apply (erule exE)
   apply (rule_tac x="pi \<bullet> pia" in exI)
@@ -138,10 +135,10 @@
   apply(erule conjE)+
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt eqvts)
+  apply(simp add: rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: eqvts atom_eqvt)
+  apply(simp add: atom_eqvt rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
   apply(simp add: permute_eqvt[symmetric])
   done