diff -r 179ff9cb160b -r 5b25fee0362c doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Wed Mar 04 10:43:39 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Wed Mar 04 10:45:52 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Doc/antiquote_setup.ML
-    ID:         $Id$
     Author:     Makarius
 
 Auxiliary antiquotations for the Isabelle manuals.
@@ -13,13 +12,17 @@
 
 (* misc utils *)
 
-val clean_string = translate_string
+fun translate f = Symbol.explode #> map f #> implode;
+
+val clean_string = translate
   (fn "_" => "\\_"
+    | "#" => "\\#"
     | "<" => "$<$"
     | ">" => "$>$"
-    | "#" => "\\#"
     | "{" => "\\{"
+    | "|" => "$\\mid$"
     | "}" => "\\}"
+    | "\\<dash>" => "-"
     | c => c);
 
 fun clean_name "\\<dots>" = "dots"
@@ -28,7 +31,7 @@
   | clean_name "_" = "underscore"
   | clean_name "{" = "braceleft"
   | clean_name "}" = "braceright"
-  | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
+  | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
 
 
 (* verbatim text *)
@@ -66,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}"
@@ -193,6 +197,7 @@
   entity_antiqs no_check "" "case" @
   entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
   entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
+  entity_antiqs no_check "" "inference" @
   entity_antiqs no_check "isatt" "executable" @
   entity_antiqs (K check_tool) "isatt" "tool" @
   entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @