| changeset 79364 | fc45f5cfb025 |
| parent 79363 | 2c6f355e52bb |
| child 79365 | b5853d438dbe |
--- 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