diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -107,7 +107,7 @@
 
 hide_const Pow
 
-datatype_new expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
+datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   | Minus expr expr | Uminus expr | Pow expr int | Exp expr
 
 text {*
@@ -197,7 +197,7 @@
 
 section {* Example negation *}
 
-datatype_new abc = A | B | C
+datatype abc = A | B | C
 
 inductive notB :: "abc => bool"
 where