--- a/Quot/Nominal/LamEx.thy	Mon Feb 01 18:57:20 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 01 18:57:39 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
 
@@ -584,25 +572,25 @@
 apply(induct t rule: lam_induct)
 apply(simp add: var_supp)
 apply(simp add: app_supp)
-apply(subgoal_tac "supp (Lam name lam) = supp (Abst {atom name} lam)")
-apply(simp add: supp_Abst)
+apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)")
+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
 
 lemma lam_supp2:
-  shows "supp (Lam x t) = supp (Abst {atom x} t)"
+  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:
   shows "supp (Lam x t) = ((supp t) - {atom x})"
 apply(simp add: lam_supp2)
-apply(simp add: supp_Abst)
+apply(simp add: supp_Abs)
 done
 
 lemma fresh_lam: