src/Pure/drule.ML

 
 (*Reset Var indexes to zero, renaming to preserve distinctness*)
 fun zero_var_indexes_list [] = []
   | zero_var_indexes_list ths =
       let
-        val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+        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;