changeset 42288 | 2074b31650e6 |
parent 42287 | d98eb048a2e4 |
child 42290 | b1f544c84040 |
--- a/src/HOL/Import/proof_kernel.ML Fri Apr 08 14:20:57 2011 +0200 +++ b/src/HOL/Import/proof_kernel.ML Fri Apr 08 15:02:11 2011 +0200 @@ -182,7 +182,7 @@ fun mk_syn thy c = if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn - else Delimfix (Syntax.escape c) + else Delimfix (Syntax_Ext.escape c) fun quotename c = if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c