src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML

             in
               if prems = [@{term False}] then
                 []
               else
                 mk_primcorec_disc_iff_tac lthy (ctr_no + 1) (the_single exhaust_thms) discs
-                  disc_excludess
+                  (flat disc_excludess)
                 |> K |> Goal.prove lthy [] [] goal
                 |> Thm.close_derivation
                 |> single
             end;