diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Thu Nov 30 13:56:46 2000 +0100
@@ -3,8 +3,7 @@
 \def\isabellecontext{pairs}%
 %
 \begin{isamarkuptext}%
-\label{sec:pairs}\indexbold{product type}
-\index{pair|see{product type}}\index{tuple|see{product type}}
+\label{sec:pairs}\indexbold{pair}
 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and