src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

                   else
                     Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                       (fn {context = ctxt, prems = _} =>
                          mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
                            (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
-                           rel_distinct_thms)
+                           rel_distinct_thms (map rel_eq_of_bnf live_nesting_bnfs))
                     |> Conjunction.elim_balanced (length goals)
                     |> Proof_Context.export names_lthy lthy
                     |> map Thm.close_derivation
                 end;
 

                     []
                   else
                     Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                       (fn {context = ctxt, prems = _} =>
                          mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms
-                           (flat sel_thmss))
+                           (flat sel_thmss) (map map_id0_of_bnf live_nesting_bnfs))
                     |> Conjunction.elim_balanced (length goals)
                     |> Proof_Context.export names_lthy lthy
                     |> map Thm.close_derivation
                 end;