src/HOL/ex/Fundefs.thy

 where
   "f3 x = finite x"
 
 
 (* Simple Higher-Order Recursion *)
-datatype 'a tree = 
+datatype_new 'a tree = 
   Leaf 'a 
   | Branch "'a tree list"
 
 fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
 where

 | "diag True True True = 4"
 | "diag False False False = 5"
 
 
 (* Many equations (quadratic blowup) *)
-datatype DT = 
+datatype_new DT = 
   A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
 | Q | R | S | T | U | V
 
 fun big :: "DT \<Rightarrow> nat"
 where