src/HOL/Finite.thy

--- a/src/HOL/Finite.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Finite.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -18,7 +18,7 @@
 syntax finite :: 'a set => bool
 translations  "finite A"  ==  "A : Finites"
 
-axclass	finite<term
+axclass	finite < type
   finite "finite UNIV"
 
 (* This definition, although traditional, is ugly to work with