prove lemma finite in context of finite class

--- a/src/HOL/Finite_Set.thy	Tue Jul 01 20:10:59 2008 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 01 20:26:48 2008 +0200
@@ -429,9 +429,14 @@
 setup {* Sign.parent_path *}
 hide const finite
 
-lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
+context finite
+begin
+
+lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
+end
+
 lemma UNIV_unit [noatp]:
   "UNIV = {()}" by auto