--- a/Nominal/Ex/Let.thy	Wed Sep 29 06:45:01 2010 -0400
+++ b/Nominal/Ex/Let.thy	Wed Sep 29 09:47:26 2010 -0400
@@ -30,13 +30,6 @@
 thm trm_assn.fresh
 thm trm_assn.exhaust
 
-
-lemma fin_bn:
-  shows "finite (set (bn l))"
-  apply(induct l rule: trm_assn.inducts(2))
-  apply(simp_all)
-  done
-
 primrec
   permute_bn_raw
 where