--- a/src/Pure/consts.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/consts.ML Thu Sep 09 12:33:14 2021 +0200
@@ -227,9 +227,8 @@
val declT = type_scheme consts c;
val args = typargs consts (c, declT);
val inst =
- 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)]);
+ TVars.build (fold2 (fn a => fn T => 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;
fun dummy_types consts =