# HG changeset patch
# User blanchet
# Date 1444336881 -7200
# Node ID 4a47a4c3e8d5dd8946df31d3c4a26ad0fa2bb34e
# Parent  76ac925927aa9ff7b4aaf1f156085b212dd13038
tuning

diff -r 76ac925927aa -r 4a47a4c3e8d5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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;