1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Wed Apr 18 17:44:39 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Thu Apr 19 07:25:41 2012 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4  %pos int
     1.5  %eop EOF
     1.6  %noshift EOF
     1.7 -%arg (file_name) : string
     1.8 +%arg (this_file_name) : string
     1.9  
    1.10  %nonassoc LET
    1.11  %nonassoc RPAREN
    1.12 @@ -247,22 +247,22 @@
    1.13                    | cnf_annotated (( cnf_annotated ))
    1.14  
    1.15  thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
    1.16 -  Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
    1.17 +  Annotated_Formula ((this_file_name, THFleft + 1, THFright + 1),
    1.18     THF, name, formula_role, thf_formula, annotations)
    1.19  ))
    1.20  
    1.21  tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
    1.22 -  Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
    1.23 +  Annotated_Formula ((this_file_name, TFFleft + 1, TFFright + 1),
    1.24     TFF, name, formula_role, tff_formula, annotations)
    1.25  ))
    1.26  
    1.27  fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
    1.28 -  Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
    1.29 +  Annotated_Formula ((this_file_name, FOFleft + 1, FOFright + 1),
    1.30     FOF, name, formula_role, fof_formula, annotations)
    1.31  ))
    1.32  
    1.33  cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
    1.34 -  Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
    1.35 +  Annotated_Formula ((this_file_name, CNFleft + 1, CNFright + 1),
    1.36     CNF, name, formula_role, cnf_formula, annotations)
    1.37  ))
    1.38  
    1.39 @@ -791,7 +791,8 @@
    1.40  useful_info : general_list (( general_list ))
    1.41  
    1.42  include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
    1.43 -  Include (file_name, formula_selection)
    1.44 +  Include ((this_file_name, INCLUDEleft + 1, INCLUDEright + 1),
    1.45 +    file_name, formula_selection)
    1.46  ))
    1.47  
    1.48  formula_selection : COMMA LBRKT name_list RBRKT   (( name_list  ))