# 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