1.1 --- a/doc-src/antiquote_setup.ML	Wed Jun 10 11:29:57 2009 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Wed Jun 10 11:31:26 2009 +0200
     1.3 @@ -19,16 +19,16 @@
     1.4      | "{" => "\\{"
     1.5      | "|" => "$\\mid$"
     1.6      | "}" => "\\}"
     1.7 -    | "\\<dash>" => "-"
     1.8 +    | "\<dash>" => "-"
     1.9      | c => c);
    1.10  
    1.11 -fun clean_name "\\<dots>" = "dots"
    1.12 +fun clean_name "\<dots>" = "dots"
    1.13    | clean_name ".." = "ddot"
    1.14    | clean_name "." = "dot"
    1.15    | clean_name "_" = "underscore"
    1.16    | clean_name "{" = "braceleft"
    1.17    | clean_name "}" = "braceright"
    1.18 -  | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
    1.19 +  | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
    1.20  
    1.21  
    1.22  (* verbatim text *)