src/HOL/Nitpick_Examples/Manual_Nits.thy

--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Oct 10 16:41:19 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Oct 10 17:43:23 2012 +0200
@@ -94,8 +94,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"