--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Apr 01 10:51:29 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Apr 01 10:51:29 2014 +0200
@@ -1675,7 +1675,7 @@
fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy =>
bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (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
((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels)
lthy;