diff -r 1d80798e8d8a -r b27bbb021df1 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -95,7 +95,7 @@
 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
 
 definition "three = {0\<Colon>nat, 1, 2}"
-typedef (open) three = three
+typedef three = three
   unfolding three_def by blast
 
 definition A :: three where "A \<equiv> Abs_three 0"
@@ -201,7 +201,7 @@
 (* BEGIN LAZY LIST SETUP *)
 definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
 
-typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
+typedef 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
 unfolding llist_def by auto
 
 definition LNil where