diff -r ec949d7206bb -r 7553a1bcecb7 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Sat Sep 13 18:08:45 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Sun Sep 14 22:59:30 2014 +0200
@@ -1,4 +1,3 @@
-
 (* Author: Lukas Bulwahn, TU Muenchen *)
 
 header {* Lazy sequences *}
@@ -9,7 +8,7 @@
 
 subsection {* Type of lazy sequences *}
 
-datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
+datatype (plugins only: code) (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
 
 primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
 where
@@ -27,11 +26,6 @@
   "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
   by (auto intro: lazy_sequence_eqI)
 
-lemma size_lazy_sequence_eq [code]:
-  "size_lazy_sequence f xq = Suc (size_list f (list_of_lazy_sequence xq))"
-  "size xq = Suc (length (list_of_lazy_sequence xq))"
-  by (cases xq, simp)+
-
 lemma case_lazy_sequence [simp]:
   "case_lazy_sequence f xq = f (list_of_lazy_sequence xq)"
   by (cases xq) auto
@@ -72,12 +66,6 @@
   case_list g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
   by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
 
-lemma size_lazy_sequence_code [code]:
-  "size_lazy_sequence s xq = (case yield xq of
-    None \<Rightarrow> 1
-  | Some (x, xq') \<Rightarrow> Suc (s x + size_lazy_sequence s xq'))"
-  by (cases "list_of_lazy_sequence xq") (simp_all add: size_lazy_sequence_eq)
-
 lemma equal_lazy_sequence_code [code]:
   "HOL.equal xq yq = (case (yield xq, yield yq) of
     (None, None) \<Rightarrow> True