# HG changeset patch
# User wenzelm
# Date 1701803272 -3600
# Node ID cfe9953696558886fce3bd27c17de3a70bb341da
# Parent  6d3322477cfd72e1913c718edd4008ea2922350d
more zproofs;

diff -r 6d3322477cfd -r cfe995369655 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 05 19:52:57 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 05 20:07:52 2023 +0100
@@ -1703,8 +1703,11 @@
       val prop' = generalize prop;
       val tpairs' = map (apply2 generalize) tpairs;
       val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
+
+      val prf = Proofterm.generalize_proof (tfrees, frees) idx prop;
+      val zprf = ZTerm.generalize_proof (tfrees, frees) idx;
     in
-      Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop, ZTerm.todo_proof) der,
+      Thm (deriv_rule1 (prf, zprf) der,
        {cert = cert,
         tags = [],
         maxidx = maxidx',
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;