src/HOL/Tools/BNF/bnf_gfp.ML

         val (Jbnfs, lthy) =
           fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
               fn consts => fn lthy =>
             bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
               (SOME deads) map_b rel_b set_bs consts lthy
-            |> register_bnf (Local_Theory.full_name lthy b))
+            |> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
           bs tacss map_bs rel_bs set_bss wit_thmss
           ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
           lthy;
 
         val timer = time (timer "registered new codatatypes as BNFs");