src/HOL/BNF/Tools/bnf_comp.ML

     fun map_cong_tac _ =
       mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
 
     val set_bd_tacs =
       if ! quick_and_dirty then
-        replicate (length set_alt_thms) (K all_tac)
+        replicate ilive (K all_tac)
       else
         let
           val outer_set_bds = set_bd_of_bnf outer;
           val inner_set_bdss = map set_bd_of_bnf inners;
           val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;