1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 18 17:44:39 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Thu Apr 19 07:25:41 2012 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4    datatype tptp_line =
     1.5        Annotated_Formula of position * language * string * role *
     1.6          tptp_formula * annotation option
     1.7 -   |  Include of string * string list
     1.8 +   |  Include of position * string * string list
     1.9  
    1.10    type tptp_problem = tptp_line list
    1.11  
    1.12 @@ -143,6 +143,8 @@
    1.13  
    1.14    val nameof_tff_atom_type : tptp_type -> string
    1.15  
    1.16 +  val pos_of_line : tptp_line -> position
    1.17 +
    1.18    (*Returns the list of all files included in a directory and its
    1.19    subdirectories. This is only used for testing the parser/interpreter against
    1.20    all THF problems.*)
    1.21 @@ -275,7 +277,7 @@
    1.22  
    1.23  datatype tptp_line =
    1.24      Annotated_Formula of position * language * string * role * tptp_formula * annotation option
    1.25 - |  Include of string * string list
    1.26 + |  Include of position * string * string list
    1.27  
    1.28  type tptp_problem = tptp_line list
    1.29  
    1.30 @@ -284,6 +286,11 @@
    1.31  fun nameof_tff_atom_type (Atom_type str) = str
    1.32    | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
    1.33  
    1.34 +fun pos_of_line tptp_line =
    1.35 +  case tptp_line of
    1.36 +      Annotated_Formula (position, _, _, _, _, _) => position
    1.37 +   |  Include (position, _, _) => position
    1.38 +
    1.39  (*Used for debugging. Returns all files contained within a directory or its
    1.40  subdirectories. Follows symbolic links, filters away directories.*)
    1.41  fun get_file_list path =