1.1 --- a/src/HOL/Set.thy	Wed Mar 30 11:32:51 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Mar 30 11:32:52 2011 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  subsection {* Sets as predicates *}
     1.6  
     1.7 -types 'a set = "'a \<Rightarrow> bool"
     1.8 +type_synonym 'a set = "'a \<Rightarrow> bool"
     1.9  
    1.10  definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
    1.11    "Collect P = P"