# HG changeset patch
# User wenzelm
# Date 1701873173 -3600
# Node ID 810679c5ed3c39efcecf26244782bf8403ddf26f
# Parent  99201e7b1d9416c861f2b03e758ff31d8db6a445
more zproofs;

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