diff -r 513316fd1087 -r 2ea3f7ebeccb doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Jul 12 20:46:32 1996 +0200
+++ b/doc-src/Logics/HOL.tex	Mon Jul 15 10:41:30 1996 +0200
@@ -1678,7 +1678,7 @@
   left-hand side, and all recursive calls in $r$ are of the form
   $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction
   rule for each constructor. Since these reduction rules are mainly used via
-  the implicit simpset, their identifiers may also be omitted.
+  the implicit simpset, their names may be omitted.
 \end{itemize}
 A theory file may contain any number of {\tt primrec} sections which may be
 intermixed with other declarations.