proper parsing of TSTP HOL lines default tip
authordesharna
Tue, 24 Nov 2020 19:49:59 +0100
changeset 72689 905abe2ed279
parent 72688 8cb82e7f1743
proper parsing of TSTP HOL lines
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)