diff -r f5c7375ab465 -r 3d101f2f817c Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -587,7 +587,7 @@
   then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
 qed
 
-lemma Abs_rename_list:
+lemma Abs_rename_lst:
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
   shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"