diff -r 00899500c6ca -r 392fd6c4669c src/HOL/Set.thy --- a/src/HOL/Set.thy Wed Mar 30 11:32:51 2011 +0200 +++ b/src/HOL/Set.thy Wed Mar 30 11:32:52 2011 +0200 @@ -8,7 +8,7 @@ subsection {* Sets as predicates *} -types 'a set = "'a \ bool" +type_synonym 'a set = "'a \ bool" definition Collect :: "('a \ bool) \ 'a set" where -- "comprehension" "Collect P = P"