src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Finite_Set.thy	Tue May 04 08:55:43 2010 +0200
@@ -509,13 +509,8 @@
 
 subsection {* Class @{text finite}  *}
 
-setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
 class finite =
   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
-setup {* Sign.parent_path *}
-hide_const finite
-
-context finite
 begin
 
 lemma finite [simp]: "finite (A \<Colon> 'a set)"