diff -r 2be5440f7271 -r efad0e364738 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Feb 26 21:43:26 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 26 23:05:47 2010 +0100
@@ -186,7 +186,7 @@
 
 fun mk_syn thy c =
   if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
-  else Syntax.literal c
+  else Delimfix (Syntax.escape c)
 
 fun quotename c =
   if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c