diff -r c8e93e8b3f55 -r 28a593f4b600 doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Thu Jan 12 10:53:42 1995 +0100
+++ b/doc-src/Logics/Old_HOL.tex	Fri Jan 13 02:00:43 1995 +0100
@@ -1557,6 +1557,7 @@
 
 \index{primitive recursion|)}
 \index{*primrec|)}
+\index{*datatype|)}
 
 
 \section{Inductive and coinductive definitions}