1.1 --- a/doc-src/antiquote_setup.ML	Thu May 15 20:02:39 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Thu May 15 20:02:40 2008 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4  fun clean_name "\\<dots>" = "dots"
     1.5    | clean_name ".." = "ddot"
     1.6    | clean_name "." = "dot"
     1.7 +  | clean_name "_" = "underscore"
     1.8    | clean_name "{" = "braceleft"
     1.9    | clean_name "}" = "braceright"
    1.10    | clean_name s = s |> translate_string (fn "_" => "-" | c => c);