# HG changeset patch
# User sultana
# Date 1335180203 -3600
# Node ID 3b53c944beceba5df5cdf7dea891292bc30baac7
# Parent  bfbd2d0bb34856fb47e306ea2e539703505b581d
disabled exception packaging in tptp;

diff -r bfbd2d0bb348 -r 3b53c944bece src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- 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',