src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

           derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct
             xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
             type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
 
         val rec_transfer_thmss =
-          if live = 0 then replicate nn []
-          else map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types);
+          map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types);
 
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
         val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
 
         val ((rel_induct_thmss, common_rel_induct_thms),

         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
         val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
 
         val flat_corec_thms = append oo append;
 
-        val corec_transfer_thmss =
-          if live = 0 then replicate nn []
-          else map single (derive_corec_transfer_thms lthy corecs corec_defs);
+        val corec_transfer_thmss = map single (derive_corec_transfer_thms lthy corecs corec_defs);
 
         val ((rel_coinduct_thmss, common_rel_coinduct_thms),
              (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
           if live = 0 then
             ((replicate nn [], []), ([], []))