--- a/src/HOL/Library/Bit.thy Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Bit.thy Fri Oct 12 18:58:20 2012 +0200
@@ -10,7 +10,7 @@
subsection {* Bits as a datatype *}
-typedef (open) bit = "UNIV :: bool set" ..
+typedef bit = "UNIV :: bool set" ..
instantiation bit :: "{zero, one}"
begin