tuned;

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