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