# HG changeset patch # User wenzelm # Date 1572793299 -3600 # Node ID 73f14e0b715183b9c63fb52122fe35d0c19ed4e2 # Parent 2c96e48027ebd0fa18ded1e7626ffec4fc73d230 more robust; diff -r 2c96e48027eb -r 73f14e0b7151 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Nov 03 15:48:59 2019 +0100 +++ b/src/Pure/thm.ML Sun Nov 03 16:01:39 2019 +0100 @@ -763,7 +763,7 @@ fun expose_proofs thy thms = if Proofterm.export_proof_boxes_required thy then - Proofterm.export_proof_boxes (map proof_of thms) + Proofterm.export_proof_boxes (map (proof_of o transfer thy) thms) else ();