
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 \<Rightarrow> bool"
+type_synonym 'a set = "'a \<Rightarrow> bool"
 
 definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
   "Collect P = P"




