src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Tue Mar 21 15:38:53 2006 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Mar 22 11:14:58 2006 +0100
@@ -13,10 +13,8 @@
 subsection {* Definition and basic properties *}
 
 consts Finites :: "'a set set"
-syntax
-  finite :: "'a set => bool"
-translations
-  "finite A" == "A : Finites"
+abbreviation (output)
+  "finite A = (A : Finites)"
 
 inductive Finites
   intros