# HG changeset patch
# User wenzelm
# Date 1244129497 -7200
# Node ID e8d5417a1831b5caffa08639f0015643628dac02
# Parent  d30a867a86fb3560fe7aa22206de5d406acbe155
export esc;

diff -r d30a867a86fb -r e8d5417a1831 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Jun 04 17:31:37 2009 +0200
+++ b/src/Pure/General/symbol.ML	Thu Jun 04 17:31:37 2009 +0200
@@ -59,6 +59,7 @@
   val source: {do_recover: bool} -> (string, 'a) Source.source ->
     (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
+  val esc: symbol -> string
   val escape: string -> string
   val strip_blanks: string -> string
   val bump_init: string -> string
@@ -487,7 +488,8 @@
 
 (* escape *)
 
-val escape = implode o map (fn s => if is_char s then s else "\\" ^ s) o sym_explode;
+val esc = fn s => if is_char s then s else "\\" ^ s;
+val escape = implode o map esc o sym_explode;
 
 
 (* blanks *)