# HG changeset patch
# User blanchet
# Date 1378938888 -7200
# Node ID 78fe0002024d33fb79e9f7c2a6a8dc5860521d7d
# Parent  d4191bf88529372f884d4ffaa015a89806443e38
more (co)data docs

diff -r d4191bf88529 -r 78fe0002024d src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 12 00:07:46 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 12 00:34:48 2013 +0200
@@ -514,7 +514,8 @@
 \noindent
 The main constituents of a constructor specification is the name of the
 constructor and the list of its argument types. An optional discriminator name
-can be supplied at the front to override the default name (@{text t.un_Cji}).
+can be supplied at the front to override the default name
+(@{text t.is_C\<^sub>j}).
 
 @{rail "
   @{syntax_def ctor_arg}: type | '(' name ':' type ')'
@@ -525,8 +526,8 @@
 \noindent
 In addition to the type of a constructor argument, it is possible to specify a
 name for the corresponding selector to override the default name
-(@{text t.un_C}$_{ij}$). The same selector names can be reused for several
-constructors as long as they have the same type.
+(@{text un_C\<^sub>ji}). The same selector names can be reused for several
+constructors as long as they share the same type.
 
 @{rail "
   @{syntax_def dt_sel_defaults}: '(' @'defaults' (name ':' term +) ')'