diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -190,7 +190,8 @@
       (type_parms ~~ map Logic.dest_type type_parms'')
       |> 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 instT) parm_types) ~~ insts'')
+      ((map #1 params ~~
+        map (Term_Subst.instantiateT_frees (Term_Subst.TFrees.table 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) $>