1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4    else Syntax.literal c
     1.5  
     1.6  fun quotename c =
     1.7 -  if Syntax.is_identifier c andalso not (OuterSyntax.is_keyword c) then c else quote c
     1.8 +  if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
     1.9  
    1.10  fun simple_smart_string_of_cterm ct =
    1.11      let