changeset 35390 | efad0e364738 |
parent 35232 | f588e1169c8b |
child 35742 | eb8d2f668bfc |
--- 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