more zproofs;
clarified signature;

--- a/src/Pure/proofterm.ML	Tue Dec 05 20:56:51 2023 +0100
+++ b/src/Pure/proofterm.ML	Tue Dec 05 21:27:42 2023 +0100
@@ -121,7 +121,7 @@
   val implies_intr_proof': term -> proof -> proof
   val forall_intr_proof: string * term -> typ option -> proof -> proof
   val forall_intr_proof': term -> proof -> proof
-  val varify_proof: ((string * sort) * (indexname * sort)) list -> proof -> proof
+  val varifyT_proof: ((string * sort) * (indexname * sort)) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
@@ -932,7 +932,7 @@
 
 (* varify *)
 
-fun varify_proof names prf =
+fun varifyT_proof names prf =
   let
     val tab = TFrees.make names;
     fun varify v =

--- a/src/Pure/thm.ML	Tue Dec 05 20:56:51 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 05 21:27:42 2023 +0100
@@ -1934,7 +1934,7 @@
     val (al, prop2) = Type.varify_global tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    (al, Thm (deriv_rule1 (Proofterm.varify_proof al, ZTerm.todo_proof) der,
+    (al, Thm (deriv_rule1 (Proofterm.varifyT_proof al, ZTerm.varifyT_proof al) der,
      {cert = cert,
       tags = [],
       maxidx = Int.max (0, maxidx),

--- a/src/Pure/zterm.ML	Tue Dec 05 20:56:51 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 05 21:27:42 2023 +0100
@@ -181,6 +181,7 @@
   val combination_proof: theory -> typ -> typ -> term -> term -> term -> term ->
     zproof -> zproof -> zproof
   val generalize_proof: Names.set * Names.set -> int -> zproof -> zproof
+  val varifyT_proof: ((string * sort) * (indexname * sort)) list -> zproof -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -513,4 +514,16 @@
           else raise Same.SAME;
   in Same.commit (map_proof_same typ (subst_term_same typ var)) prf end;
 
+fun varifyT_proof names prf =
+  if null names then prf
+  else
+    let
+      val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
+      val typ = subst_type_same (fn v =>
+        (case ZTVars.lookup tab v of
+          NONE => raise Same.SAME
+        | SOME w => ZTVar w));
+      val term = subst_term_same typ Same.same;
+    in Same.commit (map_proof_same typ term) prf end;
+
 end;