1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Tue Nov 19 14:11:26 2013 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue Nov 19 14:33:20 2013 +0100
     1.3 @@ -350,7 +350,7 @@
     1.4  custom names. In the example below, the familiar names @{text null}, @{text hd},
     1.5  @{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the
     1.6  default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
     1.7 -@{text list_set}, @{text list_map}, and @{text list_rel}:
     1.8 +@{text set_list}, @{text map_list}, and @{text rel_list}:
     1.9  *}
    1.10  
    1.11  (*<*)
    1.12 @@ -501,7 +501,7 @@
    1.13  reference manual \cite{isabelle-isar-ref}.
    1.14  
    1.15  The optional names preceding the type variables allow to override the default
    1.16 -names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
    1.17 +names of the set functions (@{text set1_t}, \ldots, @{text setM_t}).
    1.18  Inside a mutually recursive specification, all defined datatypes must
    1.19  mention exactly the same type variables in the same order.
    1.20  
    1.21 @@ -626,7 +626,7 @@
    1.22  \begin{itemize}
    1.23  \setlength{\itemsep}{0pt}
    1.24  
    1.25 -\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
    1.26 +\item \relax{Case combinator}: @{text t.t_case} (rendered using the familiar
    1.27  @{text case}--@{text of} syntax)
    1.28  
    1.29  \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
    1.30 @@ -638,22 +638,22 @@
    1.31  \phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
    1.32  
    1.33  \item \relax{Set functions} (or \relax{natural transformations}):
    1.34 -@{text t_set1}, \ldots, @{text t_setm}
    1.35 -
    1.36 -\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
    1.37 -
    1.38 -\item \relax{Relator}: @{text t_rel}
    1.39 -
    1.40 -\item \relax{Iterator}: @{text t_fold}
    1.41 -
    1.42 -\item \relax{Recursor}: @{text t_rec}
    1.43 +@{text set1_t}, \ldots, @{text t.setm_t}
    1.44 +
    1.45 +\item \relax{Map function} (or \relax{functorial action}): @{text t.map_t}
    1.46 +
    1.47 +\item \relax{Relator}: @{text t.rel_t}
    1.48 +
    1.49 +\item \relax{Iterator}: @{text t.t_fold}
    1.50 +
    1.51 +\item \relax{Recursor}: @{text t.t_rec}
    1.52  
    1.53  \end{itemize}
    1.54  
    1.55  \noindent
    1.56  The case combinator, discriminators, and selectors are collectively called
    1.57  \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
    1.58 -name and is normally hidden.
    1.59 +names and is normally hidden.
    1.60  *}
    1.61  
    1.62  
    1.63 @@ -810,8 +810,8 @@
    1.64  \item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
    1.65  @{thm list.sel_split_asm[no_vars]}
    1.66  
    1.67 -\item[@{text "t."}\hthm{case\_if}\rm:] ~ \\
    1.68 -@{thm list.case_if[no_vars]}
    1.69 +\item[@{text "t."}\hthm{case\_eq\_if}\rm:] ~ \\
    1.70 +@{thm list.case_eq_if[no_vars]}
    1.71  
    1.72  \end{description}
    1.73  \end{indentblock}
    1.74 @@ -1150,13 +1150,13 @@
    1.75  \noindent
    1.76  The next example features recursion through the @{text option} type. Although
    1.77  @{text option} is not a new-style datatype, it is registered as a BNF with the
    1.78 -map function @{const option_map}:
    1.79 +map function @{const map_option}:
    1.80  *}
    1.81  
    1.82      primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
    1.83        "sum_btree (BNode a lt rt) =
    1.84 -         a + the_default 0 (option_map sum_btree lt) +
    1.85 -           the_default 0 (option_map sum_btree rt)"
    1.86 +         a + the_default 0 (map_option sum_btree lt) +
    1.87 +           the_default 0 (map_option sum_btree rt)"
    1.88  
    1.89  text {*
    1.90  \noindent