diff -r 391e12ff816c -r aaa4667285c8 doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Thu Feb 26 20:41:28 2009 +0100
+++ b/doc-src/IsarRef/style.sty	Thu Feb 26 20:44:07 2009 +0100
@@ -15,7 +15,6 @@
 
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
-\newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
 
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}