--- a/src/Pure/thm.ML Wed Dec 06 15:21:00 2023 +0100
+++ b/src/Pure/thm.ML Wed Dec 06 15:32:53 2023 +0100
@@ -1811,10 +1811,15 @@
val constraints' =
TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
instT' constraints;
+
+ fun prf p =
+ Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') p;
+ fun zprf p =
+ ZTerm.instantiate_proof thy'
+ (TVars.fold (fn (v, (T, _)) => cons (v, T)) instT' [],
+ Vars.fold (fn (v, (t, _)) => cons (v, t)) inst' []) p;
in
- Thm (deriv_rule1
- (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d,
- ZTerm.todo_proof) der,
+ Thm (deriv_rule1 (prf, zprf) der,
{cert = cert',
tags = [],
maxidx = maxidx',
--- 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