src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy

 oops
 
 
 subsection {* AVL Trees *}
 
-datatype_new 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
+datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
 
 primrec set_of :: "'a tree \<Rightarrow> 'a set"
 where
 "set_of ET = {}" |
 "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"