1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Nov 19 15:43:08 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Nov 19 15:45:45 2013 +0100
     1.3 @@ -363,7 +363,7 @@
     1.4        Cons (infixr "#" 65)
     1.5  
     1.6      hide_type list
     1.7 -    hide_const Nil Cons hd tl set map list_all2 list_case list_rec
     1.8 +    hide_const Nil Cons hd tl set map list_all2
     1.9  
    1.10      context early begin
    1.11  (*>*)
    1.12 @@ -626,7 +626,7 @@
    1.13  \begin{itemize}
    1.14  \setlength{\itemsep}{0pt}
    1.15  
    1.16 -\item \relax{Case combinator}: @{text t.t_case} (rendered using the familiar
    1.17 +\item \relax{Case combinator}: @{text t.case_t} (rendered using the familiar
    1.18  @{text case}--@{text of} syntax)
    1.19  
    1.20  \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
    1.21 @@ -644,9 +644,9 @@
    1.22  
    1.23  \item \relax{Relator}: @{text t.rel_t}
    1.24  
    1.25 -\item \relax{Iterator}: @{text t.t_fold}
    1.26 -
    1.27 -\item \relax{Recursor}: @{text t.t_rec}
    1.28 +\item \relax{Iterator}: @{text t.fold_t}
    1.29 +
    1.30 +\item \relax{Recursor}: @{text t.rec_t}
    1.31  
    1.32  \end{itemize}
    1.33  
    1.34 @@ -914,7 +914,10 @@
    1.35  is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
    1.36  to register new-style datatypes as old-style datatypes.
    1.37  
    1.38 -\item \emph{The recursor @{text "t_rec"} has a different signature for nested
    1.39 +\item \emph{The constants @{text "t_case"} and @{text "t_rec"} are now called
    1.40 +@{text "case_t"} and @{text "rec_t"}.
    1.41 +
    1.42 +\item \emph{The recursor @{text "rec_t"} has a different signature for nested
    1.43  recursive datatypes.} In the old package, nested recursion through non-functions
    1.44  was internally reduced to mutual recursion. This reduction was visible in the
    1.45  type of the recursor, used by \keyw{primrec}. Recursion through functions was
    1.46 @@ -1552,9 +1555,9 @@
    1.47  \begin{itemize}
    1.48  \setlength{\itemsep}{0pt}
    1.49  
    1.50 -\item \relax{Coiterator}: @{text t_unfold}
    1.51 -
    1.52 -\item \relax{Corecursor}: @{text t_corec}
    1.53 +\item \relax{Coiterator}: @{text unfold_t}
    1.54 +
    1.55 +\item \relax{Corecursor}: @{text corec_t}
    1.56  
    1.57  \end{itemize}
    1.58  *}