diff -r 1f5a94209c97 -r 0ddc495e8b83 doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Tue May 03 10:40:24 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Tue May 03 10:52:32 1994 +0200
@@ -856,8 +856,8 @@
 
 
 \tdx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
-\tdx{fst}          fst(<a,b>) = a
-\tdx{snd}          snd(<a,b>) = b
+\tdx{fst_conv}     fst(<a,b>) = a
+\tdx{snd_conv}     snd(<a,b>) = b
 \tdx{split}        split(<a,b>, c) = c(a,b)
 
 \tdx{surjective_pairing}  p = <fst(p),snd(p)>