# HG changeset patch
# User desharna
# Date 1606243799 -3600
# Node ID 905abe2ed279971b33df840f4d83225ef12ec27b
# Parent  8cb82e7f1743365d7f3eba9ff013d4116170e960
proper parsing of TSTP HOL lines

diff -r 8cb82e7f1743 -r 905abe2ed279 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Nov 23 19:57:55 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 24 19:49:59 2020 +0100
@@ -561,7 +561,8 @@
               (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
             else
               (((num, [s]), phi), "", [])
-          | Inference_Source (rule, deps) => (((num, []), phi), rule, deps))
+          | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
+          | Introduced_Source rule => (((num, []), phi), rule, []))
       in
         [(name, role', phi, rule, map (rpair []) deps)]
       end)