diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
   manually slightly adapted.
 *}
  
-datatype Nat = Zer
+datatype_new Nat = Zer
              | Suc Nat
 
 fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
@@ -20,10 +20,10 @@
                                          Zer \<Rightarrow> Zer
                                        | Suc x' \<Rightarrow> sub x' y')"
 
-datatype Sym = N0
+datatype_new Sym = N0
              | N1 Sym
 
-datatype RE = Sym Sym
+datatype_new RE = Sym Sym
             | Or RE RE
             | Seq RE RE
             | And RE RE