diff -r 1753c57eb16c -r 66edcd52daeb src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Oct 21 09:31:19 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Oct 21 09:35:18 2013 +0200
@@ -1128,20 +1128,14 @@
 \noindent
 (No such map function is defined by the package because the type
 variable @{typ 'a} is dead in @{typ "'a ftree"}.)
-
-Using \keyw{fun} or \keyw{function}, recursion through functions can be
-expressed using $\lambda$-expressions and function application rather
-than through composition. For example:
+For convenience, recursion through functions can also be expressed using
+$\lambda$-expressions and function application rather than through composition.
+For example:
 *}
 
-    datatype_new_compat ftree
-
-text {* \blankline *}
-
-    function ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+    primrec_new ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
       "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
       "ftree_map f (FTNode g) = FTNode (\<lambda>x. ftree_map f (g x))"
-    by auto (metis ftree.exhaust)
 
 
 subsubsection {* Nested-as-Mutual Recursion
@@ -1830,8 +1824,8 @@
 text {*
 \noindent
 The map function for the function type (@{text \<Rightarrow>}) is composition
-(@{text "op \<circ>"}). For convenience, corecursion through functions can be
-expressed using $\lambda$-expressions and function application rather
+(@{text "op \<circ>"}). For convenience, corecursion through functions can
+also be expressed using $\lambda$-expressions and function application rather
 than through composition. For example:
 *}