--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
manually slightly adapted.
*}
-datatype_new Nat = Zer
+datatype 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_new Sym = N0
+datatype Sym = N0
| N1 Sym
-datatype_new RE = Sym Sym
+datatype RE = Sym Sym
| Or RE RE
| Seq RE RE
| And RE RE