src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

   let
     fun last_disc_tac iffD =
       HEADGOAL (rtac ctxt (rotate_prems ~1 exhaust_disc) THEN' assume_tac ctxt THEN'
       REPEAT_DETERM o (rotate_tac ~1 THEN' dtac ctxt (rotate_prems 1 iffD) THEN'
         assume_tac ctxt THEN' rotate_tac ~1 THEN'
-        etac ctxt (rotate_prems 1 notE) THEN' eresolve0_tac distinct_disc));
+        etac ctxt (rotate_prems 1 notE) THEN' eresolve_tac ctxt distinct_disc));
   in
     HEADGOAL Goal.conjunction_tac THEN
     REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI THEN' dtac ctxt (rel_sel RS iffD1) THEN'
       REPEAT_DETERM o (etac ctxt conjE) THEN' (assume_tac ctxt ORELSE' rtac ctxt iffI))) THEN
     TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)