uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
more robust handling of "|" within index;

--- a/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 20:41:28 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 20:44:07 2009 +0100
@@ -6,12 +6,6 @@
 %% references
 \newcommand{\secref}[1]{\S\ref{#1}}
 
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|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}}
-
 %% logical markup
 \newcommand{\strong}[1]{{\bfseries {#1}}}
 \newcommand{\qn}[1]{\emph{#1}}

--- a/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 20:41:28 2009 +0100
+++ b/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 20:44:07 2009 +0100
@@ -7,12 +7,6 @@
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|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}}

--- 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}}

--- 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}\,}}

--- a/doc-src/antiquote_setup.ML	Thu Feb 26 20:41:28 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Thu Feb 26 20:44:07 2009 +0100
@@ -16,10 +16,11 @@
 
 val clean_string = translate
   (fn "_" => "\\_"
+    | "#" => "\\#"
     | "<" => "$<$"
     | ">" => "$>$"
-    | "#" => "\\#"
     | "{" => "\\{"
+    | "|" => "$\\mid$"
     | "}" => "\\}"
     | "\\<dash>" => "-"
     | c => c);
@@ -68,8 +69,9 @@
     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     val _ = writeln (ml (txt1, txt2));
     val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
+    val kind' = if kind = "" then "ML" else "ML " ^ kind;
   in
-    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
+    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
     (txt'
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"