diff -r bbd2c7ffc02c -r 4a8743618257 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Nov 30 16:27:10 2011 +0100
@@ -95,8 +95,9 @@
 
 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
 
-typedef three = "{0\<Colon>nat, 1, 2}"
-by blast
+definition "three = {0\<Colon>nat, 1, 2}"
+typedef (open) three = three
+unfolding three_def by blast
 
 definition A :: three where "A \<equiv> Abs_three 0"
 definition B :: three where "B \<equiv> Abs_three 1"
@@ -197,7 +198,10 @@
    axiomatization. The examples also work unchanged with Lochbihler's
    "Coinductive_List" theory. *)
 
-typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
+definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
+
+typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
+unfolding llist_def by auto
 
 definition LNil where
 "LNil = Abs_llist (Inl [])"