changeset 70915 | bd4d37edfee4 |
parent 70914 | 05c4c6a99b3f |
child 71020 | 4003da7e6a79 |
--- a/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 16:16:23 2019 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 20:38:22 2019 +0200 @@ -15,7 +15,7 @@ fun export_proof thy thm = Proofterm.encode (Sign.consts_of thy) (Proofterm.reconstruct_proof thy (Thm.prop_of thm) - (Thm.standard_proof_of {full = true, expand = [Thm.raw_derivation_name thm]} thm)); + (Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm)); fun import_proof thy xml = let