src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy

 quickcheck[tester = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
 oops
 
 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"
 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"

 subsection {* IMP *}
 
 type_synonym var = nat
 type_synonym state = "int list"
 
-datatype com =
+datatype_new com =
   Skip |
   Ass var "int" |
   Seq com com |
   IF "state list" com com |
   While "state list" com

   quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
 oops
 
 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
 
 primrec