# HG changeset patch
# User wenzelm
# Date 1244626286 -7200
# Node ID d58d6acab3317c983d281ac2c42d2a8a13c76fc8
# Parent  5f1f0a20af4de3d07a7c67a4cbaca67ae73a0b54
eliminated escaped symbols;

diff -r 5f1f0a20af4d -r d58d6acab331 doc-src/antiquote_setup.ML
--- 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 *)