changeset 36960 | 01594f816e3a |
parent 36945 | 9bec62c10714 |
child 37145 | 01aa36932739 |
--- a/src/HOL/Import/proof_kernel.ML Mon May 17 15:11:25 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Mon May 17 23:54:15 2010 +0200 @@ -189,7 +189,7 @@ else Delimfix (Syntax.escape c) fun quotename c = - if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c + if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c fun simple_smart_string_of_cterm ct = let