src/HOL/Finite_Set.thy

 done
 
 
 subsection {* Class @{text finite} *}
 
-class finite (attach UNIV) =
+class finite (attach UNIV) = type +
   assumes finite: "finite UNIV"
 
 lemma finite_set: "finite (A::'a::finite set)"
   by (rule finite_subset [OF subset_UNIV finite])