Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML
\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}
\begin{document}
{\isamode
\begin{tabbing}
xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=\kill{}\hspace{-1ex}
consts\\
\>Ball\>::\ "\mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ (\mbox{$\alpha$}\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"\\
syntax\\
\>"@Ball"\>::\ "pttrn\ \mbox{$\Rightarrow$}\ \mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"\>\>\>\>\>("(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"\ 10)\\
translations\\
\>\>"\mbox{$\forall$}x\mbox{$\in$}A.\ P"\ \mbox{$\equiv$}\ "Ball\ A\ (\mbox{$\lambda$}x.\ P)"\\
defs\\
\ \ \ \ \ Ball\_def\>\>"Ball\ A\ P\ \mbox{$\equiv$}\ \mbox{$\forall$}x.\ x\mbox{$\in$}A\ \mbox{$\longrightarrow$}\ P\ x"\\
\\
\end{tabbing}}
\end{document}