src/Pure/drule.ML

--- a/src/Pure/drule.ML	Wed Sep 19 22:18:36 2018 +0200
+++ b/src/Pure/drule.ML	Thu Sep 20 22:39:39 2018 +0200
@@ -220,7 +220,8 @@
 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);