diff -r 99201e7b1d94 -r 810679c5ed3c src/Pure/zterm.ML
--- 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