--- a/src/Doc/Datatypes/Datatypes.thy Tue Jan 06 09:59:43 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jan 06 09:59:43 2015 +0100
@@ -110,7 +110,7 @@
Functions,'' describes how to specify corecursive functions using the
@{command primcorec} and @{command primcorecursive} commands.
-\item Section \ref{sec:introducing-bounded-natural-functors}, ``Introducing
+\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
Bounded Natural Functors,'' explains how to use the @{command bnf} command
to register arbitrary type constructors as BNFs.
@@ -325,7 +325,7 @@
Type constructors must be registered as BNFs to have live arguments. This is
done automatically for datatypes and codatatypes introduced by the
@{command datatype} and @{command codatatype} commands.
-Section~\ref{sec:introducing-bounded-natural-functors} explains how to
+Section~\ref{sec:registering-bounded-natural-functors} explains how to
register arbitrary type constructors as BNFs.
Here is another example that fails:
@@ -1137,7 +1137,7 @@
datatypes as new-style datatypes. If the goal is to define new-style datatypes
with nested recursion through old-style datatypes, the old-style
datatypes can be registered as a BNF
-(Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
+(Section~\ref{sec:registering-bounded-natural-functors}). If the goal is
to derive discriminators and selectors, this can be achieved using
@{command free_constructors}
(Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
@@ -2627,8 +2627,8 @@
*)
-section {* Introducing Bounded Natural Functors
- \label{sec:introducing-bounded-natural-functors} *}
+section {* Registering Bounded Natural Functors
+ \label{sec:registering-bounded-natural-functors} *}
text {*
The (co)datatype package can be set up to allow nested recursion through