src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Tue Feb 03 19:48:06 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Feb 03 21:26:21 2009 +0100
@@ -383,7 +383,7 @@
 subsection {* Class @{text finite}  *}
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
-class finite = itself +
+class finite =
   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
 setup {* Sign.parent_path *}
 hide const finite