--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Oct 08 14:18:34 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Oct 08 22:41:21 2015 +0200
@@ -2178,11 +2178,10 @@
val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
- fun define_ctrs_dtrs_for_type fp ((((((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), E), ctor),
- dtor), xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def),
- pre_set_defs), pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs),
- abs_inject), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings),
- sel_bindingss), raw_sel_default_eqs) no_defs_lthy =
+ fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
+ ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
+ abs abs_inject type_definition ctr_bindings ctr_mixfixes ctr_Tss disc_bindings sel_bindingss
+ raw_sel_default_eqs no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
@@ -2649,11 +2648,10 @@
val lthy'' = lthy'
|> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
- |> fold_map (define_ctrs_dtrs_for_type fp) (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ Es ~~ ctors ~~
- dtors ~~ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
- pre_set_defss ~~ pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rels ~~ ns ~~ kss ~~ mss ~~
- abss ~~ abs_injects ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~
- disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
+ |> @{fold_map 29} define_ctrs_dtrs_for_type fp_bnfs fp_bs fpTs Cs Es ctors dtors
+ xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs
+ xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss
+ ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss
|> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types
|> case_fp fp derive_note_induct_recs_thms_for_types
derive_note_coinduct_corecs_thms_for_types;