diff -r d52be75ae60b -r ea908185a597 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jun 06 11:53:52 2024 +0200
+++ b/src/Pure/zterm.ML	Thu Jun 06 12:42:42 2024 +0200
@@ -266,6 +266,8 @@
   val norm_type: Type.tyenv -> ztyp -> ztyp
   val norm_term: theory -> Envir.env -> zterm -> zterm
   val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof
+  val zproof_const_typargs: zproof_const -> ((indexname * sort) * ztyp) list
+  val zproof_const_args: zproof_const -> ((indexname * ztyp) * zterm) list
   type zbox = serial * (zterm * zproof)
   val zbox_ord: zbox ord
   type zboxes = zbox Ord_List.T
@@ -802,6 +804,14 @@
         if ZVars.defined tab v then tab else ZVars.update (v, ZVar v) tab));
   in ((a, A), (instT, inst)) end;
 
+fun zproof_const_typargs (((_, A), (instT, _)): zproof_const) =
+  ZTVars.build (A |> ZTVars.add_tvars) |> ZTVars.list_set
+  |> map (fn v => (v, the_default (ZTVar v) (ZTVars.lookup instT v)));
+
+fun zproof_const_args (((_, A), (_, inst)): zproof_const) =
+  ZVars.build (A |> ZVars.add_vars) |> ZVars.list_set
+  |> map (fn v => (v, the_default (ZVar v) (ZVars.lookup inst v)));
+
 fun make_const_proof (f, g) ((a, insts): zproof_const) =
   let
     val typ = subst_type_same (Same.function (fn ((x, _), _) => try f x));