Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper Thm.transfer;
authorwenzelm
Wed, 27 Dec 2023 11:10:51 +0100
changeset 79364 fc45f5cfb025
parent 79363 2c6f355e52bb
child 79365 b5853d438dbe
proper Thm.transfer;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle