diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -191,7 +191,7 @@
       |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
     val cert_inst =
       ((map #1 params ~~
-        map (Term_Subst.instantiateT_frees (Term_Subst.TFrees.table instT)) parm_types) ~~ insts'')
+        map (Term_Subst.instantiateT_frees (TFrees.make instT)) parm_types) ~~ insts'')
       |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
   in
     (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>