src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy

 setup {*
   Context.theory_map
     (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
 *}
 
-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"