diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -223,7 +223,7 @@
 
 subsection {* 2.10. Boxing *}
 
-datatype_new tm = Var nat | Lam tm | App tm tm
+datatype tm = Var nat | Lam tm | App tm tm
 
 primrec lift where
 "lift (Var j) k = Var (if j < k then j else j + 1)" |
@@ -306,7 +306,7 @@
 
 subsection {* 3.1. A Context-Free Grammar *}
 
-datatype_new alphabet = a | b
+datatype alphabet = a | b
 
 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
   "[] \<in> S\<^sub>1"
@@ -381,7 +381,7 @@
 
 subsection {* 3.2. AA Trees *}
 
-datatype_new 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
+datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
 
 primrec data where
 "data \<Lambda> = undefined" |