src/HOL/ex/Serbian.thy

--- a/src/HOL/ex/Serbian.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Serbian.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
 begin
 
 text{* Serbian cyrillic letters *}
-datatype_new azbuka =
+datatype azbuka =
   azbA   ("А")
 | azbB   ("Б")
 | azbV   ("В")
@@ -47,7 +47,7 @@
 thm azbuka.induct
 
 text{* Serbian latin letters *}
-datatype_new abeceda =
+datatype abeceda =
   abcA   ("A")
 | abcB   ("B")
 | abcC   ("C")