src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML

     Splitter.split_tac (split_if :: splits))) THEN
   mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
   HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
     SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
     (rtac refl ORELSE' atac ORELSE'
-     resolve_tac split_connectI ORELSE'
+     resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
      Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
      Splitter.split_tac (split_if :: splits) ORELSE'
      mk_primcorec_assumption_tac ctxt discIs ORELSE'
      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
      (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))));