src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML

     val (ctr, ctr_args) = strip_comb (unfold_let rhs);
     val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
       handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
 
     val disc_concl = betapply (disc, lhs);
-    val (eqn_data_disc_opt, matchedsss') = if length basic_ctr_specs = 1
-      then (NONE, matchedsss)
-      else apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos
+    val (eqn_data_disc_opt, matchedsss') =
+      if null (tl basic_ctr_specs) then
+        (NONE, matchedsss)
+      else
+        apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos
           (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss);
 
     val sel_concls = sels ~~ ctr_args
       |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
 

         val sel_thmss = map (map snd o order_list_duplicates) sel_alists;
 
         fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
             (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
-          if null exhaust_thms then
+          if null exhaust_thms orelse null (tl ctr_specs) then
             []
           else
             let
               val {disc, disc_excludess, ...} = nth ctr_specs ctr_no;
               val goal =