--- a/Quot/Nominal/Terms.thy	Wed Feb 03 12:31:58 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:44:29 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
 
@@ -646,7 +643,7 @@
 quotient_type 
   qtrm4 = trm4 / alpha4 and
   qtrm4list = "trm4 list" / alpha4list
-  by (simp_all add: alpha4_equivp alpha4list_equivp
+  by (simp_all add: alpha4_equivp alpha4list_equivp)
 
 
 datatype rtrm5 =