diff -r 1d80798e8d8a -r b27bbb021df1 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -1189,7 +1189,7 @@
   \medskip The following trivial example pulls a three-element type
   into existence within the formal logical environment of HOL. *}
 
-typedef (open) three = "{(True, True), (True, False), (False, True)}"
+typedef three = "{(True, True), (True, False), (False, True)}"
   by blast
 
 definition "One = Abs_three (True, True)"