# HG changeset patch
# User wenzelm
# Date 1703936067 -3600
# Node ID e6a12ea61f83d31446f84044eb1367f3c8592b65
# Parent  25fa3bc05a5152f536f0357e66b91038bbeda8ed
more operations;

diff -r 25fa3bc05a51 -r e6a12ea61f83 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Dec 30 12:12:43 2023 +0100
+++ b/src/Pure/zterm.ML	Sat Dec 30 12:34:27 2023 +0100
@@ -244,6 +244,9 @@
   val subst_term_bound: zterm -> zterm -> zterm
   val subst_proof_bound: zterm -> zproof -> zproof
   val subst_proof_boundp: zproof -> zproof -> zproof
+  val subst_type_same: (indexname * sort, ztyp) Same.function -> ztyp Same.operation
+  val subst_term_same:
+    ztyp Same.operation -> (indexname * ztyp, zterm) Same.function -> zterm Same.operation
   exception BAD_INST of ((indexname * ztyp) * zterm) list
   val map_proof: ztyp Same.operation -> zterm Same.operation -> zproof -> zproof
   val map_proof_types: ztyp Same.operation -> zproof -> zproof