src/Pure/drule.ML

--- a/src/Pure/drule.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/drule.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -214,11 +214,15 @@
 
         val tvars = fold Thm.add_tvars ths [];
         fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);
-        val instT' = map (fn (v, TVar (b, _)) => (v, Thm.rename_tvar b (the_tvar v))) instT;
+        val instT' =
+          (instT, []) |-> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
+            cons (v, Thm.rename_tvar b (the_tvar v)));
 
         val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths [];
         fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars);
-        val inst' = map (fn (v, Var (b, _)) => (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))) inst;
+        val inst' =
+          (inst, []) |-> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
+            cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))));
       in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
 
 val zero_var_indexes = singleton zero_var_indexes_list;