--- a/src/Pure/consts.ML Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/consts.ML Sat Sep 04 21:25:08 2021 +0200
@@ -227,8 +227,8 @@
val declT = type_scheme consts c;
val args = typargs consts (c, declT);
val inst =
- fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T))
- args Ts Term_Subst.TVars.empty
+ Term_Subst.TVars.build
+ (fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T)) args Ts)
handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
in declT |> Term_Subst.instantiateT inst end;