src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

               val rel_eq_thms =
                 map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
                 map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
                   rel_inject_thms ms;
 
-              val (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *)) =
+              val (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) =
                 let
                   val (((Ds, As), Bs), names_lthy) = lthy
                     |> mk_TFrees (dead_of_bnf fp_bnf)
                     ||>> mk_TFrees (live_of_bnf fp_bnf)
                     ||>> mk_TFrees (live_of_bnf fp_bnf);

                   val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
                   val discsA = map (mk_disc_or_sel ADs) discs;
                   val selssA = map (map (mk_disc_or_sel ADs)) selss;
                   val disc_sel_pairs = flat (map2 (map o pair) discsA selssA);
 
-(* FIXME:
                   val (rel_cases_thm, rel_cases_attrs) =
                     let
                       val rel = mk_rel_of_bnf Ds As Bs fp_bnf;
                       val (((thesis, Rs), tb), names_lthy) =  names_lthy
                         |> yield_singleton (mk_Frees "thesis") HOLogic.boolT

                       val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
                       val cases_pred_attr = Attrib.internal o K o Induct.cases_pred;
                     in
                       (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
                     end;
-*)
 
                   val disc_map_iff_thms =
                     let
                       val discsB = map (mk_disc_or_sel BDs) discs;
                       val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discsA;

                               (flat sel_thmss) set_thms)
                           |> Conjunction.elim_balanced (length goals)
                           |> Proof_Context.export names_lthy lthy
                     end;
                 in
-                  (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *))
+                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs))
                 end;
 
               val anonymous_notes =
                 [([case_cong], fundefcong_attrs),
                  (rel_eq_thms, code_nitpicksimp_attrs)]
                 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
               val notes =
                 [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
                  (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
-(* FIXME:                 (rel_casesN, [rel_cases_thm], rel_cases_attrs), *)
+                 (rel_casesN, [rel_cases_thm], rel_cases_attrs),
                  (rel_distinctN, rel_distinct_thms, simp_attrs),
                  (rel_injectN, rel_inject_thms, simp_attrs),
                  (rel_introsN, rel_intro_thms, []),
                  (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
                  (sel_mapN, sel_map_thms, []),