--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 14 11:10:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Feb 14 13:45:29 2014 +0100
@@ -2637,12 +2637,12 @@
mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
val (Jbnfs, lthy) =
- fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts =>
- fn lthy =>
+ fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms =>
+ fn consts => fn lthy =>
bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads)
map_b rel_b set_bs consts lthy
|> register_bnf (Local_Theory.full_name lthy b))
- tacss map_bs rel_bs set_bss Jwit_thmss
+ bs tacss map_bs rel_bs set_bss Jwit_thmss
((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels)
lthy;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Feb 14 11:10:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Feb 14 13:45:29 2014 +0100
@@ -1730,11 +1730,11 @@
mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
val (Ibnfs, lthy) =
- fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy =>
+ 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) I tacs wit_tac (SOME deads)
map_b rel_b set_bs consts lthy
|> register_bnf (Local_Theory.full_name lthy b))
- tacss map_bs rel_bs set_bss
+ bs tacss map_bs rel_bs set_bss
((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels)
lthy;