diff -r f5d79aeffd81 -r b5e6122ff575 doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Thu Nov 13 21:48:19 2008 +0100
+++ b/doc-src/IsarRef/style.sty	Thu Nov 13 21:49:46 2008 +0100
@@ -17,7 +17,7 @@
 \newcommand{\Figref}[1]{Figure~\ref{#1}}
 
 %% ML
-\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
+\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
 \newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
 
 %% math