# HG changeset patch
# User wenzelm
# Date 1703155243 -3600
# Node ID 30eed4e3baddda87f08b730a409972137e11237f
# Parent  b03e22697999414e08f9f7f60d7e5ca8b8d9a3a5
tuned;

diff -r b03e22697999 -r 30eed4e3badd src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Dec 20 22:32:57 2023 +0100
+++ b/src/Pure/zterm.ML	Thu Dec 21 11:40:43 2023 +0100
@@ -496,8 +496,8 @@
             NONE => I
           | SOME t' => ZVars.update (v, t')))
       else
-        ZVars.dest inst
-        |> map (fn (v, t) => (the_default v (ZVars.lookup vars' v), the_default t (apply term t)))
+        build (inst |> ZVars.fold_rev (fn (v, t) =>
+          cons (the_default v (ZVars.lookup vars' v), the_default t (apply term t))))
         |> make_inst;
   in if ! changed then (instT', inst') else raise Same.SAME end;