# HG changeset patch
# User wenzelm
# Date 1703672096 -3600
# Node ID b5853d438dbec86bf39cd64a745633cefe04ff45
# Parent  fc45f5cfb025daf26e73b9875e464699830afe58
more operations;

diff -r fc45f5cfb025 -r b5853d438dbe src/Pure/thm.ML
--- 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});