# HG changeset patch
# User sultana
# Date 1378241201 -3600
# Node ID b6fd2f4414620d4ef40217c940126842b4cfce03
# Parent  51b562922cb17fbce407ffba3782e1806505f457
now allowing numeric identifiers to be used in 'file' annotations;
more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;

diff -r 51b562922cb1 -r b6fd2f441462 src/HOL/TPTP/TPTP_Parser/tptp_proof.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Tue Sep 03 21:46:40 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Tue Sep 03 21:46:41 2013 +0100
@@ -49,6 +49,8 @@
 
 open TPTP_Syntax
 
+exception ANNOT_STRUCTURE of general_term
+
 (*Extract name of inference rule, and the inferences it relies on*)
 (*This is tuned to work with LEO-II, and is brittle wrt upstream
   changes of the proof protocol.*)
@@ -119,6 +121,15 @@
               General_Data (Atomic_Word defname)])), _) =
                 (SOME (File (filename, defname)))
 
+      | analyse_annot
+         (General_Data
+           (Application
+             ("file",
+              [General_Data (Atomic_Word filename),
+               General_Data (Number (Int_num, defname))])), _) =
+                (SOME (File (filename, defname)))
+
+      | analyse_annot (other, _) = raise (ANNOT_STRUCTURE other)
   in
     case annot of
       NONE => NONE