diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -53,7 +53,7 @@
 
 section {* Context Free Grammar *}
 
-datatype alphabet = a | b
+datatype_new 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 com =
+datatype_new com =
   Skip |
   Ass var "int" |
   Seq com com |
@@ -206,11 +206,11 @@
 
 subsection {* Lambda *}
 
-datatype type =
+datatype_new type =
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 
-datatype dB =
+datatype_new dB =
     Var nat
   | App dB dB (infixl "\<degree>" 200)
   | Abs type dB