1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Mon Apr 23 12:23:23 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Mon Apr 23 12:23:23 2012 +0100
     1.3 @@ -836,7 +836,7 @@
     1.4       | integer     (( integer ))
     1.5  
     1.6  atomic_word : LOWER_WORD    (( LOWER_WORD ))
     1.7 -            | SINGLE_QUOTED (( SINGLE_QUOTED ))
     1.8 +            | SINGLE_QUOTED (( dequote SINGLE_QUOTED ))
     1.9              | THF           (( "thf" ))
    1.10              | TFF           (( "tff" ))
    1.11              | FOF           (( "fof" ))