--- 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