1.1 --- a/doc-src/ZF/FOL.tex	Mon May 30 15:30:05 2011 +0100
     1.2 +++ b/doc-src/ZF/FOL.tex	Mon May 30 16:10:12 2011 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  \begin{center}
     1.5  \index{*"= symbol}
     1.6  \index{&@{\tt\&} symbol}
     1.7 -\index{*"| symbol}
     1.8 +\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
     1.9  \index{*"-"-"> symbol}
    1.10  \index{*"<"-"> symbol}
    1.11  \begin{tabular}{rrrr}