src/HOL/Nitpick_Examples/Manual_Nits.thy

 sorry
 
 
 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)" |
 "lift (Lam t) k = Lam (lift t (k + 1))" |
 "lift (App t u) k = App (lift t k) (lift u k)"

 nitpick_params [max_potential = 0]
 
 
 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"
 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"

 sorry
 
 
 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" |
 "data (N x _ _ _) = x"