src/Doc/Datatypes/Datatypes.thy

 
 \item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
 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.
 
 \item Section
 \ref{sec:deriving-destructors-and-theorems-for-free-constructors},

 @{typ 'b} is live.
 
 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:
 *}
 

 
 In the other direction, there is currently no way to register old-style
 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}).
 *}
 

 partial_function to the rescue
 *}
 *)
 
 
-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
 arbitrary type constructors, as long as they adhere to the BNF requirements
 and are registered as BNFs. It is also possible to declare a BNF abstractly