# 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 ();