# HG changeset patch
# User wenzelm
# Date 1157737483 -7200
# Node ID 99ad217b6974c15e61774f81c45b3e43001c48d3
# Parent  48fea5e99505e97959f073a2cf0a7b18e8528aa1
tuned;

diff -r 48fea5e99505 -r 99ad217b6974 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Fri Sep 08 17:33:05 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Fri Sep 08 19:44:43 2006 +0200
@@ -81,35 +81,34 @@
 
   A \emph{type constructor} \isa{{\isasymkappa}} is a \isa{k}-ary operator
   on types declared in the theory.  Type constructor application is
-  usually written postfix as \isa{{\isacharparenleft}FIXME{\isacharparenright}{\isasymkappa}}.  For \isa{k\ {\isacharequal}\ {\isadigit{0}}}
-  the argument tuple is omitted, e.g.\ \isa{prop} instead of
-  \isa{{\isacharparenleft}{\isacharparenright}prop}.  For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses are omitted,
-  e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}.  Further
-  notation is provided for specific constructors, notably
-  right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun} constructor.
+  usually written postfix as \isa{{\isacharparenleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub k{\isacharparenright}{\isasymkappa}}.
+  For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}.  For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the
+  parentheses are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}.  Further notation is provided for specific constructors,
+  notably the right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of
+  \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}.
   
   A \emph{type} is defined inductively over type variables and type
-  constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}.
+  constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}k}.
 
-  A \emph{type abbreviation} is a syntactic abbreviation of an
-  arbitrary type expression of the theory.  Type abbreviations looks
-  like type constructors at the surface, but are expanded before the
-  core logic encounters them.
+  A \emph{type abbreviation} is a syntactic abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} of an arbitrary type expression \isa{{\isasymtau}} over
+  variables \isa{\isactrlvec {\isasymalpha}}.  Type abbreviations looks like type
+  constructors at the surface, but are fully expanded before entering
+  the logical core.
 
   A \emph{type arity} declares the image behavior of a type
-  constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is
-  of sort \isa{s} if each argument type \isa{{\isasymtau}\isactrlisub i} is of
-  sort \isa{s\isactrlisub i}.  Arity declarations are implicitly
-  completed, i.e.\ \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}.
+  constructor wrt.\ the algebra of sorts: \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}{\isasymkappa}} is
+  of sort \isa{s} if every argument type \isa{{\isasymtau}\isactrlisub i} is
+  of sort \isa{s\isactrlisub i}.  Arity declarations are implicitly
+  completed, i.e.\ \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}.
 
   \medskip The sort algebra is always maintained as \emph{coregular},
   which means that type arities are consistent with the subclass
-  relation: for each type constructor \isa{c} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts.
+  relation: for each type constructor \isa{{\isasymkappa}} and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds componentwise.
 
   The key property of a coregular order-sorted algebra is that sort
-  constraints may be always fulfilled in a most general fashion: for
-  each type constructor \isa{c} and sort \isa{s} there is a
-  most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}c} is
+  constraints may be always solved in a most general fashion: for each
+  type constructor \isa{{\isasymkappa}} and sort \isa{s} there is a most
+  general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}{\isasymkappa}} is
   of sort \isa{s}.  Consequently, the unification problem on the
   algebra of types has most general solutions (modulo renaming and
   equivalence of sorts).  Moreover, the usual type-inference algorithm
@@ -127,8 +126,9 @@
 \begin{mldecls}
   \indexmltype{class}\verb|type class| \\
   \indexmltype{sort}\verb|type sort| \\
+  \indexmltype{arity}\verb|type arity| \\
   \indexmltype{typ}\verb|type typ| \\
-  \indexmltype{arity}\verb|type arity| \\
+  \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
   \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
   \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
   \indexml{Sign.add-types}\verb|Sign.add_types: (bstring * int * mixfix) list -> theory -> theory| \\
@@ -148,32 +148,35 @@
   \verb|class list|.
 
   \item \verb|arity| represents type arities; this is an alias for
-  triples of the form \isa{{\isacharparenleft}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} described above.
+  triples of the form \isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} described above.
 
   \item \verb|typ| represents types; this is a datatype with
   constructors \verb|TFree|, \verb|TVar|, \verb|Type|.
 
+  \item \verb|fold_atyps|~\isa{f\ {\isasymtau}} iterates function \isa{f}
+  over all occurrences of atoms (\verb|TFree| or \verb|TVar|) of \isa{{\isasymtau}}; the type structure is traversed from left to right.
+
   \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}}
   tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}.
 
   \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether a type
   is of a given sort.
 
-  \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new
-  type constructors \isa{c} with \isa{k} arguments and
+  \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new
+  type constructors \isa{{\isasymkappa}} with \isa{k} arguments and
   optional mixfix syntax.
 
-  \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
-  defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c\ {\isacharequal}\ {\isasymtau}} with
+  \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
+  defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} with
   optional mixfix syntax.
 
-  \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c} derived together with
-  class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}.
+  \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c}, together with class
+  relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}.
 
   \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}.
 
-  \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares
-  arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}.
+  \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares
+  arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}.
 
   \end{description}%
 \end{isamarkuptext}%
diff -r 48fea5e99505 -r 99ad217b6974 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 17:33:05 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 08 19:44:43 2006 +0200
@@ -70,45 +70,46 @@
 
   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
   on types declared in the theory.  Type constructor application is
-  usually written postfix as @{text "(FIXME)\<kappa>"}.  For @{text "k = 0"}
-  the argument tuple is omitted, e.g.\ @{text "prop"} instead of
-  @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,
-  e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further
-  notation is provided for specific constructors, notably
-  right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
-  \<beta>)fun"} constructor.
+  usually written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.
+  For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text
+  "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
+  parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text
+  "(\<alpha>)list"}.  Further notation is provided for specific constructors,
+  notably the right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of
+  @{text "(\<alpha>, \<beta>)fun"}.
   
   A \emph{type} is defined inductively over type variables and type
   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
-  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
+  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.
 
-  A \emph{type abbreviation} is a syntactic abbreviation of an
-  arbitrary type expression of the theory.  Type abbreviations looks
-  like type constructors at the surface, but are expanded before the
-  core logic encounters them.
+  A \emph{type abbreviation} is a syntactic abbreviation @{text
+  "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
+  variables @{text "\<^vec>\<alpha>"}.  Type abbreviations looks like type
+  constructors at the surface, but are fully expanded before entering
+  the logical core.
 
   A \emph{type arity} declares the image behavior of a type
-  constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
-  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
-  of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
-  sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
-  completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
+  constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
+  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
+  of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
+  of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
+  completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
 
   \medskip The sort algebra is always maintained as \emph{coregular},
   which means that type arities are consistent with the subclass
-  relation: for each type constructor @{text "c"} and classes @{text
-  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
-  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
+  relation: for each type constructor @{text "\<kappa>"} and classes @{text
+  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::
+  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>
   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
-  \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
+  \<^vec>s\<^isub>2"} holds componentwise.
 
   The key property of a coregular order-sorted algebra is that sort
-  constraints may be always fulfilled in a most general fashion: for
-  each type constructor @{text "c"} and sort @{text "s"} there is a
-  most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
+  constraints may be always solved in a most general fashion: for each
+  type constructor @{text "\<kappa>"} and sort @{text "s"} there is a most
+  general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
   s\<^isub>k)"} such that a type scheme @{text
-  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
+  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is
   of sort @{text "s"}.  Consequently, the unification problem on the
   algebra of types has most general solutions (modulo renaming and
   equivalence of sorts).  Moreover, the usual type-inference algorithm
@@ -119,8 +120,9 @@
   \begin{mldecls}
   @{index_ML_type class} \\
   @{index_ML_type sort} \\
+  @{index_ML_type arity} \\
   @{index_ML_type typ} \\
-  @{index_ML_type arity} \\
+  @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
@@ -140,36 +142,40 @@
   @{ML_type "class list"}.
 
   \item @{ML_type arity} represents type arities; this is an alias for
-  triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
+  triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
   (\<^vec>s)s"} described above.
 
   \item @{ML_type typ} represents types; this is a datatype with
   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
 
+  \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}
+  over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text
+  "\<tau>"}; the type structure is traversed from left to right.
+
   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
 
   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   is of a given sort.
 
-  \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
-  type constructors @{text "c"} with @{text "k"} arguments and
+  \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
+  type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   optional mixfix syntax.
 
-  \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
-  defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
+  \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
+  defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
   optional mixfix syntax.
 
   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
-  c\<^isub>n])"} declares new class @{text "c"} derived together with
-  class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
+  c\<^isub>n])"} declares new class @{text "c"}, together with class
+  relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
 
   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   c\<^isub>2"}.
 
-  \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
-  arity @{text "c :: (\<^vec>s)s"}.
+  \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
+  arity @{text "\<kappa> :: (\<^vec>s)s"}.
 
   \end{description}
 *}