diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -107,7 +107,7 @@
 
 hide_const Pow
 
-datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
+datatype_new 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 abc = A | B | C
+datatype_new abc = A | B | C
 
 inductive notB :: "abc => bool"
 where