--- a/src/Pure/zterm.ML Wed Dec 06 15:21:00 2023 +0100
+++ b/src/Pure/zterm.ML Wed Dec 06 15:32:53 2023 +0100
@@ -181,6 +181,8 @@
val combination_proof: theory -> typ -> typ -> term -> term -> term -> term ->
zproof -> zproof -> zproof
val generalize_proof: Names.set * Names.set -> int -> zproof -> zproof
+ val instantiate_proof: theory ->
+ ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> zproof -> zproof
val varifyT_proof: ((string * sort) * (indexname * sort)) list -> zproof -> zproof
end;
@@ -527,6 +529,17 @@
else raise Same.SAME);
in Same.commit (map_proof_same typ term) prf end;
+fun instantiate_proof thy (Ts, ts) prf =
+ let
+ val instT = ZTVars.build (Ts |> fold (fn (v, T) => ZTVars.add (v, ztyp_of T)));
+ val inst =
+ ZVars.build (ts |> fold (fn ((v, T), t) => ZVars.add ((v, ztyp_of T), global_zterm_of thy t)));
+ val typ =
+ if ZTVars.is_empty instT then Same.same
+ else subst_type_same (Same.function (ZTVars.lookup instT));
+ val term = subst_term_same typ (Same.function (ZVars.lookup inst));
+ in Same.commit (map_proof_same typ term) prf end;
+
fun varifyT_proof names prf =
if null names then prf
else