tuned;

--- a/src/Pure/zterm.ML	Wed Dec 06 16:04:00 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 19:45:53 2023 +0100
@@ -291,12 +291,6 @@
 fun map_proof_types_same typ =
   map_proof_same typ (subst_term_same typ Same.same);
 
-
-(* instantiation *)
-
-fun init_instT t = ZTVars.build (ZTVars.add_tvars t) |> ZTVars.map (fn v => fn _ => ZTVar v);
-fun init_inst t = ZVars.build (ZVars.add_vars t) |> ZVars.map (fn v => fn _ => ZVar v);
-
 fun map_const_proof (f, g) prf =
   (case prf of
     ZConstP (a, A, instT, inst) =>
@@ -375,8 +369,8 @@
 fun const_proof thy a A =
   let
     val t = global_zterm_of thy A;
-    val instT = init_instT t;
-    val inst = init_inst t;
+    val instT = ZTVars.build (ZTVars.add_tvars t) |> ZTVars.map (fn v => fn _ => ZTVar v);
+    val inst = ZVars.build (ZVars.add_vars t) |> ZVars.map (fn v => fn _ => ZVar v);
   in ZConstP (a, t, instT, inst) end;
 
 fun axiom_proof thy name = const_proof thy (ZAxiom name);