# HG changeset patch
# User wenzelm
# Date 1702493750 -3600
# Node ID 46d16fc4bc151e7c64733fd4424064218e940ec8
# Parent  479f31c4b3673f3cc9f006bca21dcd32ed6bb385
tuned signature;

diff -r 479f31c4b367 -r 46d16fc4bc15 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Dec 13 15:23:03 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 13 19:55:50 2023 +0100
@@ -167,6 +167,8 @@
   val incr_bv_same: int -> int -> zterm Same.operation
   val incr_bv: int -> int -> zterm -> zterm
   val incr_boundvars: int -> zterm -> zterm
+  val map_proof_same: ztyp Same.operation -> zterm Same.operation -> zproof Same.operation
+  val map_proof_types_same: ztyp Same.operation -> zproof Same.operation
   val ztyp_of: typ -> ztyp
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
   val zterm_of: theory -> term -> zterm