diff -r 6d3322477cfd -r cfe995369655 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 05 19:52:57 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 05 20:07:52 2023 +0100
@@ -180,6 +180,7 @@
   val abstract_rule_proof: theory -> typ -> typ -> string * term -> term -> term -> zproof -> zproof
   val combination_proof: theory -> typ -> typ -> term -> term -> term -> term ->
     zproof -> zproof -> zproof
+  val generalize_proof: Names.set * Names.set -> int -> zproof -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -495,4 +496,21 @@
 
 end;
 
+
+(* substitution *)
+
+fun generalize_proof (tfrees, frees) idx prf =
+  let
+    val typ =
+      if Names.is_empty tfrees then Same.same else
+        subst_type_same (fn ((a, i), S) =>
+          if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S)
+          else raise Same.SAME);
+    val var =
+      if Names.is_empty frees then Same.same else
+        fn ((x, i), T) =>
+          if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
+          else raise Same.SAME;
+  in Same.commit (map_proof_same typ (subst_term_same typ var)) prf end;
+
 end;