src/HOL/TPTP/TPTP_Parser/tptp.lex

--- a/src/HOL/TPTP/TPTP_Parser/tptp.lex	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.lex	Thu Aug 07 12:17:41 2014 +0200
@@ -86,6 +86,7 @@
 upper_word                = {upper_alpha}{alpha_numeric}*;
 dollar_dollar_word        = {ddollar}{lower_word};
 dollar_word               = {dollar}{lower_word};
+dollar_underscore         = {dollar}_;
 
 distinct_object           = {double_quote}{do_char}+{double_quote};
 
@@ -177,6 +178,7 @@
 
 {lower_word}   => (col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col));
 {dollar_word}  => (col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col));
+{dollar_underscore}  => (col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col));
 {dollar_dollar_word}  => (col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col));
 
 "+"           => (col:=yypos-(!eolpos); T.PLUS(!linep,!col));