diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -53,7 +53,7 @@
 
 section {* Context Free Grammar *}
 
-datatype_new alphabet = a | b
+datatype alphabet = a | b
 
 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
   "[] \<in> S\<^sub>1"
@@ -179,7 +179,7 @@
 type_synonym var = nat
 type_synonym state = "int list"
 
-datatype_new com =
+datatype com =
   Skip |
   Ass var "int" |
   Seq com com |
@@ -206,11 +206,11 @@
 
 subsection {* Lambda *}
 
-datatype_new type =
+datatype type =
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 
-datatype_new dB =
+datatype dB =
     Var nat
   | App dB dB (infixl "\<degree>" 200)
   | Abs type dB