diff -r 1da96affdefe -r ec3fc818b82e doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Fri Feb 13 19:41:14 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Sat Feb 14 21:34:12 2009 +0100
@@ -12,13 +12,16 @@
 
 (* misc utils *)
 
-val clean_string = translate_string
+fun translate f = Symbol.explode #> map f #> implode;
+
+val clean_string = translate
   (fn "_" => "\\_"
     | "<" => "$<$"
     | ">" => "$>$"
     | "#" => "\\#"
     | "{" => "\\{"
     | "}" => "\\}"
+    | "\\<dash>" => "-"
     | c => c);
 
 fun clean_name "\\<dots>" = "dots"
@@ -27,7 +30,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 *)