--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 09 20:51:36 2014 +0200
@@ -223,7 +223,7 @@
subsection {* 2.10. Boxing *}
-datatype tm = Var nat | Lam tm | App tm tm
+datatype_new 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 alphabet = a | b
+datatype_new 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 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
+datatype_new 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
primrec data where
"data \<Lambda> = undefined" |