diff -r c25ff084868f -r ee0619b5adff Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Fri Jan 29 07:09:52 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Sat Jan 30 11:44:25 2010 +0100
@@ -584,25 +584,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 (Abs {atom name} lam)")
-apply(simp add: supp_Abs)
+apply(subgoal_tac "supp (Lam name lam) = supp (Abst {atom name} lam)")
+apply(simp add: supp_Abst)
 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 apply(simp add: Lam_pseudo_inject)
-apply(simp add: abs_eq)
+apply(simp add: abs_eq alpha_gen)
 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
 done
 
 lemma lam_supp2:
-  shows "supp (Lam x t) = supp (Abs {atom x} t)"
+  shows "supp (Lam x t) = supp (Abst {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)
-sorry
+apply(simp add: abs_eq 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_Abs)
+apply(simp add: supp_Abst)
 done
 
 lemma fresh_lam: