--- a/doc-src/antiquote_setup.ML Wed Jun 10 11:29:57 2009 +0200
+++ b/doc-src/antiquote_setup.ML Wed Jun 10 11:31:26 2009 +0200
@@ -19,16 +19,16 @@
| "{" => "\\{"
| "|" => "$\\mid$"
| "}" => "\\}"
- | "\\<dash>" => "-"
+ | "\<dash>" => "-"
| c => c);
-fun clean_name "\\<dots>" = "dots"
+fun clean_name "\<dots>" = "dots"
| clean_name ".." = "ddot"
| clean_name "." = "dot"
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
- | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
+ | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
(* verbatim text *)