src/Doc/Datatypes/Datatypes.thy

       "tree\<^sub>i\<^sub>i_of_stream s =
          Node\<^sub>i\<^sub>i (shd s) (lmap tree\<^sub>i\<^sub>i_of_stream (LCons (stl s) LNil))"
 
 text {*
 \noindent
-A more natural syntax, also supported by Isabelle, is to move corecursive calls
-under constructors:
-*}
-
-    primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
+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}:
+*}
+
+    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
 special. Deterministic finite automata (DFAs) are traditionally defined as
 5-tuples @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,