src/Pure/zterm.ML

--- 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;