--- a/Quot/Nominal/LFex.thy	Wed Feb 03 12:45:06 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 03 12:58:02 2010 +0100
@@ -652,15 +652,15 @@
 apply(simp add: KIND_TY_TRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
-apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
+apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
 apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
 apply(simp add: KIND_TY_TRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
 apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
 apply(simp add: supp_Abs Set.Un_commute)
@@ -668,7 +668,7 @@
 apply(simp add: KIND_TY_TRM_INJECT)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts atom_eqvt)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
 done