diff -r 8dd0e0316881 -r c830ead80c91 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 06 12:47:50 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 06 13:00:16 2013 +0100
@@ -1847,12 +1847,14 @@
 
 text {*
 \noindent
-A more natural syntax, also supported by Isabelle, is to move corecursive calls
-under constructors:
+Fortunately, it is easy to prove the following lemma, where the corecursive call
+is moved inside the lazy list constructor, thereby eliminating the need for
+@{const lmap}:
 *}
 
-    primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
+    lemma tree\<^sub>i\<^sub>i_of_stream_alt:
       "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)"
+    by (subst tree\<^sub>i\<^sub>i_of_stream.code) simp
 
 text {*
 The next example illustrates corecursion through functions, which is a bit