changeset 70914 | 05c4c6a99b3f |
parent 70839 | 2136e4670ad2 |
child 70915 | bd4d37edfee4 |
--- a/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 12:56:36 2019 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 16:16:23 2019 +0200 @@ -14,7 +14,8 @@ ML \<open> fun export_proof thy thm = Proofterm.encode (Sign.consts_of thy) - (Proofterm.reconstruct_proof thy (Thm.prop_of thm) (Thm.standard_proof_of true thm)); + (Proofterm.reconstruct_proof thy (Thm.prop_of thm) + (Thm.standard_proof_of {full = true, expand = [Thm.raw_derivation_name thm]} thm)); fun import_proof thy xml = let