diff -r 3740fb5ec307 -r 8e6b2ad9cfe0 src/HOL/TPTP/TPTP_Parser/tptp_proof.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Wed Feb 19 15:57:02 2014 +0000
@@ -113,6 +113,7 @@
                        (inference_name,
                         analyse_useful_info useful_info [],
                         analyse_parent_info parent_info [])))
+
       | analyse_annot
          (General_Data
           (Application
@@ -129,6 +130,17 @@
                General_Data (Number (Int_num, defname))])), _) =
                 (SOME (File (filename, defname)))
 
+      (*This was added to support Satallax proofs.*)
+      | analyse_annot
+         (General_Data
+           (Application
+             ("introduced",
+              [General_Data (Atomic_Word "assumption"),
+               General_List []])), _) =
+                (SOME (Inference
+                       ("assumption", [], [])))
+
+
       | analyse_annot (other, _) = raise (ANNOT_STRUCTURE other)
   in
     case annot of