--- 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',