1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 06 12:47:50 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 06 13:00:16 2013 +0100
     1.3 @@ -1847,12 +1847,14 @@
     1.4  
     1.5  text {*
     1.6  \noindent
     1.7 -A more natural syntax, also supported by Isabelle, is to move corecursive calls
     1.8 -under constructors:
     1.9 +Fortunately, it is easy to prove the following lemma, where the corecursive call
    1.10 +is moved inside the lazy list constructor, thereby eliminating the need for
    1.11 +@{const lmap}:
    1.12  *}
    1.13  
    1.14 -    primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
    1.15 +    lemma tree\<^sub>i\<^sub>i_of_stream_alt:
    1.16        "tree\<^sub>i\<^sub>i_of_stream s = Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
    1.17 +    by (subst tree\<^sub>i\<^sub>i_of_stream.code) simp
    1.18  
    1.19  text {*
    1.20  The next example illustrates corecursion through functions, which is a bit