--- a/src/Doc/Logics/document/HOL.tex Wed Feb 12 08:35:57 2014 +0100
+++ b/src/Doc/Logics/document/HOL.tex Wed Feb 12 08:35:57 2014 +0100
@@ -1231,7 +1231,7 @@
Note that Isabelle insists on precisely this format; you may not even change
the order of the two cases.
Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
-\cdx{nat_rec}, which is available because \textit{nat} is represented as
+\cdx{rec_nat}, which is available because \textit{nat} is represented as
a datatype.
%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.