src/HOL/BNF/Tools/bnf_gfp.ML

               |> Thm.close_derivation
           end;
 
         val timer = time (timer "map functions for the new codatatypes");
 
-        val bd = mk_cexp sbd sbd;
-
-        val timer = time (timer "bounds for the new codatatypes");
-
         val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks;
         val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks;
         val setss_by_range = transpose setss_by_bnf;
 
         val dtor_set_thmss =

         val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms;
         val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
         val set_nat_tacss =
           map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss);
 
-        val bd_co_tacs = replicate n (K (mk_bd_card_order_tac sbd_card_order));
-        val bd_cinf_tacs = replicate n (K (mk_bd_cinfinite_tac sbd_Cinfinite));
+        val bd_co_tacs = replicate n (K (rtac sbd_card_order 1));
+        val bd_cinf_tacs = replicate n (K (rtac (sbd_Cinfinite RS conjunct1) 1));
 
         val set_bd_tacss =
           map2 (map2 (K oo mk_set_bd_tac sbd_Cinfinite)) hset_defss (transpose col_bd_thmss);
 
         val map_wpull_tacs =

         val (Jbnfs, lthy) =
           fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
               fn T => fn (thms, wits) => fn lthy =>
             bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b
               rel_b set_bs
-              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), bd), wits), NONE) lthy
+              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);