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