--- a/src/Pure/thm.ML Wed Dec 27 11:10:51 2023 +0100
+++ b/src/Pure/thm.ML Wed Dec 27 11:14:56 2023 +0100
@@ -173,6 +173,7 @@
val varifyT_global: thm -> thm
val legacy_freezeT: thm -> thm
val plain_prop_of: thm -> term
+ val get_zproof_serials: theory -> serial list
val get_zproof: theory -> serial -> {name: Thm_Name.T * Position.T, thm: thm} option
val store_zproof: Thm_Name.T * Position.T -> thm -> theory -> thm * theory
val dest_state: thm * int -> (term * term) list * term list * term * term
@@ -2076,6 +2077,8 @@
(* stored thms: zproof *)
+val get_zproof_serials = Inttab.keys o get_zproofs;
+
fun get_zproof thy =
Inttab.lookup (get_zproofs thy)
#> Option.map (fn {name, thm} => {name = name, thm = transfer thy thm});