more robust;
authorwenzelm
Sun, 03 Nov 2019 16:01:39 +0100
changeset 71012 73f14e0b7151
parent 71011 2c96e48027eb
child 71013 bfa1017b4553
more robust;
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 ();