src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy

 
 section {* Example symbolic derivation *}
 
 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 {*
 
 d(U + V, X, DU + DV) :-

 values_prolog "{e. log10 e}"
 values_prolog "{e. times10 e}"
 
 section {* Example negation *}
 
-datatype_new abc = A | B | C
+datatype abc = A | B | C
 
 inductive notB :: "abc => bool"
 where
   "y \<noteq> B \<Longrightarrow> notB y"