# HG changeset patch
# User wenzelm
# Date 1701888878 -3600
# Node ID e47db1e15a2215f46ae6427c55beda982639dfb1
# Parent  16a144eaf67dbe3f9d47601de40321a41b96ad42
minor performance tuning;

diff -r 16a144eaf67d -r e47db1e15a22 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Dec 06 19:45:53 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 19:54:38 2023 +0100
@@ -369,8 +369,14 @@
 fun const_proof thy a A =
   let
     val t = global_zterm_of thy A;
-    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);
+    val instT =
+      ZTVars.build (t |> (fold_types o fold_tvars) (fn v => fn tab =>
+        if ZTVars.defined tab v then tab else ZTVars.update (v, ZTVar v) tab));
+    val inst =
+      ZVars.build (t |> fold_aterms (fn a => fn tab =>
+        (case a of
+          ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, a) tab
+        | _ => tab)));
   in ZConstP (a, t, instT, inst) end;
 
 fun axiom_proof thy name = const_proof thy (ZAxiom name);