diff -r 98c8b7542b72 -r fce9d97a3258 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 18 17:44:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Thu Apr 19 07:25:41 2012 +0100
@@ -131,7 +131,7 @@
   datatype tptp_line =
       Annotated_Formula of position * language * string * role *
         tptp_formula * annotation option
-   |  Include of string * string list
+   |  Include of position * string * string list
 
   type tptp_problem = tptp_line list
 
@@ -143,6 +143,8 @@
 
   val nameof_tff_atom_type : tptp_type -> string
 
+  val pos_of_line : tptp_line -> position
+
   (*Returns the list of all files included in a directory and its
   subdirectories. This is only used for testing the parser/interpreter against
   all THF problems.*)
@@ -275,7 +277,7 @@
 
 datatype tptp_line =
     Annotated_Formula of position * language * string * role * tptp_formula * annotation option
- |  Include of string * string list
+ |  Include of position * string * string list
 
 type tptp_problem = tptp_line list
 
@@ -284,6 +286,11 @@
 fun nameof_tff_atom_type (Atom_type str) = str
   | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
 
+fun pos_of_line tptp_line =
+  case tptp_line of
+      Annotated_Formula (position, _, _, _, _, _) => position
+   |  Include (position, _, _) => position
+
 (*Used for debugging. Returns all files contained within a directory or its
 subdirectories. Follows symbolic links, filters away directories.*)
 fun get_file_list path =