src/Pure/drule.ML

         val (instT, inst) =
           Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths);
 
         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;