diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -187,14 +187,15 @@
 
     (* instantiation *)
     val instT =
-      (type_parms ~~ map Logic.dest_type type_parms'')
-      |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
+      TFrees.build
+        (fold2 (fn v => fn T => not (TFree v = T) ? TFrees.add (v, T))
+          type_parms (map Logic.dest_type type_parms''));
     val cert_inst =
-      ((map #1 params ~~
-        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));
+      Frees.build
+        (fold2 (fn v => fn t => not (Free v = t) ? Frees.add (v, cert t))
+          (map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) insts'');
   in
-    (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
+    (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $>
       Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
   end;