doc-src/HOL/HOL.tex

--- a/doc-src/HOL/HOL.tex	Mon May 30 15:30:05 2011 +0100
+++ b/doc-src/HOL/HOL.tex	Mon May 30 16:10:12 2011 +0100
@@ -67,7 +67,7 @@
 \begin{constants}
 \index{*"= symbol}
 \index{&@{\tt\&} symbol}
-\index{*"| symbol}
+\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
 \index{*"-"-"> symbol}
   \it symbol    & \it meta-type & \it priority & \it description \\ 
   \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &