--- a/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 17:08:36 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Feb 17 17:21:43 2016 +0100
@@ -1429,16 +1429,7 @@
text \<open>
\noindent
-For convenience, the predicator can be used instead of the map function,
-typically when defining predicates. For example:
-\<close>
-
-primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
- "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow> n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
-
-text \<open>
-\noindent
-Also for convenience, recursion through functions can also be expressed using
+For convenience, recursion through functions can also be expressed using
$\lambda$-abstractions and function application rather than through composition.
For example:
\<close>
@@ -1478,6 +1469,14 @@
primrec (nonexhaustive) subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
"subtree_ft2 x y (FTNode2 g) = g x y"
+text \<open>
+For any datatype featuring nesting, the predicator can be used instead of the
+map function, typically when defining predicates. For example:
+\<close>
+
+ primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
+ "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow> n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
+
subsubsection \<open> Nested-as-Mutual Recursion
\label{sssec:primrec-nested-as-mutual-recursion} \<close>