src/HOL/Import/proof_kernel.ML
changeset 35390 efad0e364738
parent 35232 f588e1169c8b
child 35742 eb8d2f668bfc
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Feb 26 21:43:26 2010 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 26 23:05:47 2010 +0100
     1.3 @@ -186,7 +186,7 @@
     1.4  
     1.5  fun mk_syn thy c =
     1.6    if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
     1.7 -  else Syntax.literal c
     1.8 +  else Delimfix (Syntax.escape c)
     1.9  
    1.10  fun quotename c =
    1.11    if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c