tuned;

--- a/doc-src/Ref/simplifier.tex	Thu Oct 29 14:32:43 1998 +0100
+++ b/doc-src/Ref/simplifier.tex	Thu Oct 29 15:05:42 1998 +0100
@@ -690,8 +690,7 @@
 \begin{ttbox}
 by (simp_tac (simpset() addloop ("split if",split_tac [split_if])) 1);
 \end{ttbox}
-Users would usually prefer the following shortcut using
-\ttindex{addsplits}:
+Users would usually prefer the following shortcut using \texttt{addsplits}:
 \begin{ttbox}
 by (simp_tac (simpset() addsplits [split_if]) 1);
 \end{ttbox}