--- a/Quot/Nominal/LamEx.thy	Mon Feb 01 16:05:59 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 01 20:02:44 2010 +0100
@@ -47,18 +47,6 @@
 unfolding fresh_star_def
 by (simp add: fresh_plus)
 
-lemma supp_finite_set:
-  fixes S::"atom set"
-  assumes "finite S"
-  shows "supp S = S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
-  apply(metis)
-  apply(rule assms)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
-done
-  
 
 atom_decl name
 
@@ -588,7 +576,7 @@
 apply(simp add: supp_Abs)
 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 apply(simp add: Lam_pseudo_inject)
-apply(simp add: abs_eq alpha_gen)
+apply(simp add: Abs_eq_iff alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
 done
 
@@ -596,7 +584,7 @@
   shows "supp (Lam x t) = supp (Abs {atom x} t)"
 apply(simp add: supp_def permute_set_eq atom_eqvt)
 apply(simp add: Lam_pseudo_inject)
-apply(simp add: abs_eq supp_fv alpha_gen)
+apply(simp add: Abs_eq_iff supp_fv alpha_gen)
 done
 
 lemma lam_supp: