diff -r f5417836dbea -r 01594f816e3a src/HOL/Import/proof_kernel.ML
--- 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