diff -r c0de5386017e -r f3b4fde34cd1 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Mon Oct 18 12:33:13 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Mon Oct 18 15:35:20 2010 +0100
@@ -136,17 +136,17 @@
 
   \begin{description}
 
-  \item @{ML_type class} represents type classes.
+  \item Type @{ML_type class} represents type classes.
 
-  \item @{ML_type sort} represents sorts, i.e.\ finite intersections
-  of classes.  The empty list @{ML "[]: sort"} refers to the empty
-  class intersection, i.e.\ the ``full sort''.
+  \item Type @{ML_type sort} represents sorts, i.e.\ finite
+  intersections of classes.  The empty list @{ML "[]: sort"} refers to
+  the empty class intersection, i.e.\ the ``full sort''.
 
-  \item @{ML_type arity} represents type arities.  A triple @{text
-  "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> :: (\<^vec>s)s"} as
-  described above.
+  \item Type @{ML_type arity} represents type arities.  A triple
+  @{text "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> ::
+  (\<^vec>s)s"} as described above.
 
-  \item @{ML_type typ} represents types; this is a datatype with
+  \item Type @{ML_type typ} represents types; this is a datatype with
   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
 
   \item @{ML Term.map_atyps}~@{text "f \<tau>"} applies the mapping @{text
@@ -374,8 +374,8 @@
 
   \begin{description}
 
-  \item @{ML_type term} represents de-Bruijn terms, with comments in
-  abstractions, and explicitly named free variables and constants;
+  \item Type @{ML_type term} represents de-Bruijn terms, with comments
+  in abstractions, and explicitly named free variables and constants;
   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
   Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
 
@@ -653,8 +653,8 @@
 
   \begin{description}
 
-  \item @{ML_type ctyp} and @{ML_type cterm} represent certified types
-  and terms, respectively.  These are abstract datatypes that
+  \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified
+  types and terms, respectively.  These are abstract datatypes that
   guarantee that its values have passed the full well-formedness (and
   well-typedness) checks, relative to the declarations of type
   constructors, constants etc. in the theory.
@@ -668,8 +668,8 @@
   reasoning loops.  There are separate operations to decompose
   certified entities (including actual theorems).
 
-  \item @{ML_type thm} represents proven propositions.  This is an
-  abstract datatype that guarantees that its values have been
+  \item Type @{ML_type thm} represents proven propositions.  This is
+  an abstract datatype that guarantees that its values have been
   constructed by basic principles of the @{ML_struct Thm} module.
   Every @{ML_type thm} value contains a sliding back-reference to the
   enclosing theory, cf.\ \secref{sec:context-theory}.