src/HOL/Lazy_Sequence.thy

--- a/src/HOL/Lazy_Sequence.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
 
 subsection {* Type of lazy sequences *}
 
-datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
+datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
 
 primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
 where