--- a/doc-src/Ref/defining.tex Tue May 20 10:44:45 1997 +0200
+++ b/doc-src/Ref/defining.tex Tue May 20 10:47:56 1997 +0200
@@ -689,8 +689,8 @@
of mathematical symbols from a special screen font instead of {\sc
ascii}. Another example is to re-use Isabelle's advanced
$\lambda$-term printing mechanisms to generate completely different
-output, say for interfacing external tools like model checkers (see
-also \texttt{HOL/Modelcheck}).
+output, say for interfacing external tools like \rmindex{model
+ checkers} (see also \texttt{HOL/Modelcheck}).
\index{print modes|)}