src/Doc/Logics/document/HOL.tex

--- a/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:56 2014 +0100
@@ -1435,7 +1435,7 @@
 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b
 \end{center}
 is defined by translation.  For details see~{\S}\ref{sec:HOL:datatype}. There
-is also a case splitting rule \tdx{split_list_case}
+is also a case splitting rule \tdx{list.split}
 \[
 \begin{array}{l}
 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~