--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Apr 01 10:51:29 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Apr 01 10:51:29 2014 +0200
@@ -2433,10 +2433,10 @@
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 =>
+ fn consts =>
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
- |> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
+ (SOME deads) map_b rel_b set_bs consts
+ #> (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;
--- 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
@@ -1672,10 +1672,10 @@
mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
val (Ibnfs, lthy) =
- fold_map6 (fn b => 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 =>
bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
- map_b rel_b set_bs consts lthy
- |> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
+ map_b rel_b set_bs consts
+ #> (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;