diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Normalization_by_Evaluation.thy
--- a/src/HOL/ex/Normalization_by_Evaluation.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -15,7 +15,7 @@
 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
 lemma "~((0::nat) < (0::nat))" by normalization
 
-datatype n = Z | S n
+datatype_new n = Z | S n
 
 primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
    "add Z = id"