author | wenzelm |
Sun, 03 Nov 2019 16:01:39 +0100 | |
changeset 71012 | 73f14e0b7151 |
parent 71011 | 2c96e48027eb |
child 71013 | bfa1017b4553 |
src/Pure/thm.ML | file | annotate | diff | comparison | revisions |
--- 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 ();