src/HOL/Tools/BNF/bnf_comp_tactics.ML

 val cprod_thms =
   @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
 
 val simplified_set_simps =
   @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
-    o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_comp_def};
+    o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_def};
 
 fun mk_simplified_set_tac ctxt collect_set_map =
   unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
   unfold_thms_tac ctxt simplified_set_simps THEN rtac refl 1;