# 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)