--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Apr 23 12:23:23 2012 +0100
@@ -805,6 +805,7 @@
(*process the line, ignoring the type-context for variables*)
val ((type_map', const_map', l'), thy') =
interpret_line config inc_list type_map const_map path_prefix line thy
+ (*FIXME
handle
(*package all exceptions to include position information,
even relating to multiple levels of "include"ed files*)
@@ -815,6 +816,7 @@
(TPTP_Syntax.pos_of_line line :: pos_list, exn)
| exn => raise MISINTERPRET
([TPTP_Syntax.pos_of_line line], exn)
+ *)
in
((type_map',
const_map',