src/Pure/Isar/object_logic.ML

 fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
 fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
 
 fun gen_rulify full ctxt =
   Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
-  #> Drule.gen_all #> Thm.strip_shyps #> Drule.zero_var_indexes;
+  #> Drule.gen_all (Variable.maxidx_of ctxt)
+  #> Thm.strip_shyps
+  #> Drule.zero_var_indexes;
 
 val rulify = gen_rulify true;
 val rulify_no_asm = gen_rulify false;
 
 val rule_format = Thm.rule_attribute (rulify o Context.proof_of);