diff -r 207a7811faa9 -r 99224854a0ac doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Sun Nov 02 13:47:58 1997 +0100
+++ b/doc-src/Logics/HOL.tex	Sun Nov 02 14:01:38 1997 +0100
@@ -1632,7 +1632,7 @@
 \end{warn}
 
 To perform case distinction on a goal containing a \texttt{case}-construct,
-the theorem \texttt{split_}$t$\texttt{_case} is provided:
+the theorem \texttt{split_}$t$\texttt{_case}\tdx{split_$t$_case} is provided:
 \[
 \begin{array}{@{}rcl@{}}
 P(t_\mathtt{case}~f@1~\dots~f@m~e) &=&