src/HOL/Lazy_Sequence.thy

--- a/src/HOL/Lazy_Sequence.thy	Tue Sep 16 18:42:33 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Tue Sep 16 19:23:37 2014 +0200
@@ -8,7 +8,8 @@
 
 subsection {* Type of lazy sequences *}
 
-datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
+datatype (plugins only: code extraction) (dead 'a) lazy_sequence =
+  lazy_sequence_of_list "'a list"
 
 primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
 where