--- a/doc-src/Ref/syntax.tex Thu Apr 13 15:01:11 2000 +0200
+++ b/doc-src/Ref/syntax.tex Thu Apr 13 15:01:35 2000 +0200
@@ -890,7 +890,7 @@
\begin{ttbox}
val token_translation:
(string * string * (string -> string * real)) list
-\end{ttbox}\index{token_translation}
+\end{ttbox}
The elements of this list are of the form $(m, c, f)$, where $m$ is a print
mode identifier, $c$ a token class, and $f\colon string \to string \times
real$ the actual translation function. Assuming that $x$ is of identifier