src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -517,6 +517,9 @@
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
+lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
+  by simp
+
 end
 
 lemma UNIV_unit [no_atp]: