# HG changeset patch
# User traytel
# Date 1392381929 -3600
# Node ID 6ec4d06297a5e11dbe8ce75ff893aad90ccab4fa
# Parent  e2cf2df4fd83bf1c357011f3fb63193ac67dd605
register bnfs for (co)datatypes under their proper name (lost in af71b753c459)

diff -r e2cf2df4fd83 -r 6ec4d06297a5 src/HOL/Tools/BNF/bnf_gfp.ML
--- 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;
 
diff -r e2cf2df4fd83 -r 6ec4d06297a5 src/HOL/Tools/BNF/bnf_lfp.ML
--- 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;