Typography: extra space between '\index{...} \index{...}' removed.

Manual/Description/theories.tex

@@ -801,7 +801,10 @@ \subsection{Pairs}\label{prod}
 \end{verbatim}
 \end{hol}
 %
-The type operator {\small\verb%prod%} is defined by invoking \ml{new\_type\_definition}\index{new_type_definition@\ml{new\_type\_definition}} with this theorem which results in the definitional axiom \index{axioms!non-primitive, of HOL logic@non-primitive, of \HOL{} logic!for products} \index{axioms!in bool theory@in \ml{bool} theory} \ml{prod\_TY\_DEF} shown below being asserted in the theory \ml{pair}.
+The type operator {\small\verb%prod%} is defined by invoking \ml{new\_type\_definition}\index{new_type_definition@\ml{new\_type\_definition}} with this theorem which results in the definitional axiom
+\index{axioms!non-primitive, of HOL logic@non-primitive, of \HOL{} logic!for products}%
+\index{axioms!in bool theory@in \ml{bool} theory}%
+\ml{prod\_TY\_DEF} shown below being asserted in the theory \ml{pair}.
 %
 \begin{hol}
 \begin{verbatim}