--- a/Nominal/Abs.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -447,8 +447,9 @@
 
 lemma Abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  by (lifting alpha_abs.simps(1))
-
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+  by (lifting alphas_abs)
 
 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>
   prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"

--- a/Nominal/Fv.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -896,7 +896,7 @@
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW

--- a/Nominal/Nominal2_FSet.thy	Sat Mar 27 09:15:09 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Sat Mar 27 09:21:43 2010 +0100
@@ -44,7 +44,7 @@
 
 end
 
-lemma permute_fset[simp,eqvt]:
+lemma permute_fset[eqvt]:
   "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
   "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
   by (lifting permute_list.simps)