src/Doc/Datatypes/Datatypes.thy

 The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
 the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
 variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
 
 The optional names preceding the type variables allow to override the default
-names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Type
+names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
 arguments can be marked as dead by entering ``@{text dead}'' in front of the
 type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
 (and a set function is generated or not) depending on where they occur in the
 right-hand sides of the definition. Declaring a type argument as dead can speed
 up the type definition but will prevent any later (co)recursion through that

 
 \begin{tabular}{@ {}ll@ {}}
 Case combinator: &
   @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
 Discriminators: &
-  @{text "t.is_C\<^sub>1"}$, \ldots, $@{text "t.is_C\<^sub>n"} \\
+  @{text t.is_C\<^sub>1}$, \ldots, $@{text t.is_C\<^sub>n} \\
 Selectors: &
   @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
 & \quad\vdots \\
 & @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
 Set functions: &
-  @{text t.set1_t}, \ldots, @{text t.setm_t} \\
+  @{text t.set\<^sub>1_t}, \ldots, @{text t.set\<^sub>m_t} \\
 Map function: &
   @{text t.map_t} \\
 Relator: &
   @{text t.rel_t} \\
 Recursor: &

 
 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.set(1)[no_vars]} \\
 @{thm list.set(2)[no_vars]}
 
-\item[@{text "t."}\hthm{set_cases}\rm:] ~ \\
+\item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
 @{thm list.set_cases[no_vars]}
 
 \item[@{text "t."}\hthm{set_empty}\rm:] ~ \\
 @{thm list.set_empty[no_vars]}