# HG changeset patch
# User wenzelm
# Date 1703671851 -3600
# Node ID fc45f5cfb025daf26e73b9875e464699830afe58
# Parent  2c6f355e52bba1474279d3ed7db4bdfc450e80cd
proper Thm.transfer;

diff -r 2c6f355e52bb -r fc45f5cfb025 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 26 22:14:44 2023 +0100
+++ b/src/Pure/thm.ML	Wed Dec 27 11:10:51 2023 +0100
@@ -2076,7 +2076,9 @@
 
 (* stored thms: zproof *)
 
-val get_zproof = Inttab.lookup o get_zproofs;
+fun get_zproof thy =
+  Inttab.lookup (get_zproofs thy)
+  #> Option.map (fn {name, thm} => {name = name, thm = transfer thy thm});
 
 fun store_zproof name thm thy =
   let