src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML

     val (ms', f_ctrs') =
       (case maybe_nchotomy of
         NONE => (ms, f_ctrs)
       | SOME nchotomy =>
         (ms |> split_last ||> K [n - 1] |> op @,
-         f_ctrs |> split_last ||> (fn thm => [rulify_nchotomy n nchotomy RS thm]) |> op @));
+         f_ctrs
+         |> split_last
+         ||> unfold_thms ctxt @{thms atomize_conjL}
+         ||> (fn thm => [rulify_nchotomy n nchotomy RS thm])
+         |> op @));
   in
     EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
       ms' f_ctrs') THEN
     IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
       HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))