src/HOL/Library/Saturated.thy

--- a/src/HOL/Library/Saturated.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Saturated.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
 
 subsection {* The type of saturated naturals *}
 
-typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef ('a::len) sat = "{.. len_of TYPE('a)}"
   morphisms nat_of Abs_sat
   by auto