diff -r 391e12ff816c -r aaa4667285c8 doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Thu Feb 26 20:41:28 2009 +0100
+++ b/doc-src/IsarImplementation/style.sty	Thu Feb 26 20:44:07 2009 +0100
@@ -7,13 +7,6 @@
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
-\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
-\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
-\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
-\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
-
 %% math
 \newcommand{\text}[1]{\mbox{#1}}
 \newcommand{\isasymvartheta}{\isamath{\theta}}