src/HOL/ZF/Zet.thy

--- a/src/HOL/ZF/Zet.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/ZF/Zet.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -11,7 +11,7 @@
 
 definition "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
 
-typedef (open) 'a zet = "zet :: 'a set set"
+typedef 'a zet = "zet :: 'a set set"
   unfolding zet_def by blast
 
 definition zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool" where