src/Provers/classical.ML

             hyp :: hyps => exists (fn t => t aconv hyp) hyps
           | _ => false);
       val rule'' =
         rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
           if i = 1 orelse redundant_hyp goal
-          then eresolve0_tac [thin_rl] i
+          then eresolve_tac ctxt [thin_rl] i
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;
     in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
   else rule;