src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy

--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -132,7 +132,7 @@
 
 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