more zproofs;

--- a/src/Pure/thm.ML	Wed Dec 06 15:58:20 2023 +0100
+++ b/src/Pure/thm.ML	Wed Dec 06 16:04:00 2023 +0100
@@ -1958,8 +1958,10 @@
     val prop1 = attach_tpairs tpairs prop;
     val prop2 = Type.legacy_freeze prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
+    fun prf p = Proofterm.legacy_freezeT prop1 p;
+    fun zprf p = ZTerm.legacy_freezeT_proof prop1 p;
   in
-    Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1, ZTerm.todo_proof) der,
+    Thm (deriv_rule1 (prf, zprf) der,
      {cert = cert,
       tags = [],
       maxidx = maxidx_of_term prop2,

--- a/src/Pure/zterm.ML	Wed Dec 06 15:58:20 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 16:04:00 2023 +0100
@@ -184,6 +184,7 @@
   val instantiate_proof: theory ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> zproof -> zproof
   val varifyT_proof: ((string * sort) * (indexname * sort)) list -> zproof -> zproof
+  val legacy_freezeT_proof: term -> zproof -> zproof
   val incr_indexes_proof: int -> zproof -> zproof
 end;
 
@@ -553,6 +554,15 @@
           | SOME w => ZTVar w));
     in Same.commit (map_proof_types_same typ) prf end;
 
+fun legacy_freezeT_proof t prf =
+  (case Type.legacy_freezeT t of
+    NONE => prf
+  | SOME f =>
+      let
+        val tvar = ztyp_of o Same.function f;
+        val typ = subst_type_same tvar;
+      in Same.commit (map_proof_types_same typ) prf end);
+
 fun incr_indexes_proof inc prf =
   let
     fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME;