diff -r 1dd314a00b0c -r 4239a0784e5f Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Mon Feb 01 15:57:37 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 01 16:05:59 2010 +0100
@@ -584,8 +584,8 @@
 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)
@@ -593,7 +593,7 @@
 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)
@@ -602,7 +602,7 @@
 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: