src/HOL/BNF/Tools/bnf_gfp.ML

 
           fun mk_in_sbd i Co Cnz bd =
             Cnz RS ((@{thm ordLeq_ordIso_trans} OF
               [(Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})), sbd_ordIso]) RS
               (bd RS @{thm ordLeq_transitive[OF _
-                cexp_mono2_Cnotzero[OF _ csum_Cnotzero2[OF ctwo_Cnotzero]]]}));
+                cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
           val in_sbds = map4 mk_in_sbd ks bd_Card_orders bd_Cnotzeros in_bds;
        in
          (lthy, sbd, sbdT,
            sbd_card_order, sbd_Cinfinite, sbd_Cnotzero, sbd_Card_order, set_sbdss, in_sbds)
        end;