--- 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) $>