--- 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