src/HOL/Library/RBT.thy

--- a/src/HOL/Library/RBT.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/RBT.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
 
 subsection {* Type definition *}
 
-typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+typedef ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
   morphisms impl_of RBT
 proof -
   have "RBT_Impl.Empty \<in> ?rbt" by simp