src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy

 text {* An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"}) *}
 text {* The example (original in Haskell) was imported with Haskabelle and
   manually slightly adapted.
 *}
  
-datatype_new Nat = Zer
+datatype Nat = Zer
              | Suc Nat
 
 fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
 where
   "sub x y = (case y of
                  Zer \<Rightarrow> x
                | Suc y' \<Rightarrow> case x of
                                          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
             | Star RE
             | Empty