# HG changeset patch
# User blanchet
# Date 1367221514 -7200
# Node ID 67757f1d5e7151baf7e909164429b978fc730c44
# Parent  be6e703908f4c6d8c62415cb6a83d7662814e05e
use record instead of huge tuple

diff -r be6e703908f4 -r 67757f1d5e71 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 09:10:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 09:45:14 2013 +0200
@@ -8,8 +8,21 @@
 signature BNF_FP =
 sig
   type fp_result =
-    BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
-      thm list * thm list * thm list * thm list list * thm list * thm list * thm list
+    {bnfs : BNF_Def.BNF list,
+     dtors : term list,
+     ctors : term list,
+     folds : term list,
+     recs : term list,
+     induct : thm,
+     strong_induct : thm,
+     dtor_ctors : thm list,
+     ctor_dtors : thm list,
+     ctor_injects : thm list,
+     map_thms : thm list,
+     set_thmss : thm list list,
+     rel_thms : thm list,
+     fold_thms : thm list,
+     rec_thms : thm list}
 
   val time: Timer.real_timer -> string -> Timer.real_timer
 
@@ -155,8 +168,21 @@
 open BNF_Util
 
 type fp_result =
-  BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
-    thm list * thm list * thm list * thm list list * thm list * thm list * thm list;
+  {bnfs : BNF_Def.BNF list,
+   dtors : term list,
+   ctors : term list,
+   folds : term list,
+   recs : term list,
+   induct : thm,
+   strong_induct : thm,
+   dtor_ctors : thm list,
+   ctor_dtors : thm list,
+   ctor_injects : thm list,
+   map_thms : thm list,
+   set_thmss : thm list list,
+   rel_thms : thm list,
+   fold_thms : thm list,
+   rec_thms : thm list};
 
 val timing = true;
 fun time timer msg = (if timing
diff -r be6e703908f4 -r 67757f1d5e71 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 09:10:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 09:45:14 2013 +0200
@@ -255,10 +255,10 @@
     val fp_eqs =
       map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
 
-    (* TODO: clean up list *)
-    val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
-           fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
-           fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
+    val (pre_bnfs, ({bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0,
+           folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
+           dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
+           rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms}, lthy)) =
       fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
         no_defs_lthy0;
 
diff -r be6e703908f4 -r 67757f1d5e71 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Apr 29 09:10:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Apr 29 09:45:14 2013 +0200
@@ -3029,9 +3029,12 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((Jbnfs, dtors, ctors, unfolds, corecs, dtor_coinduct_thm, dtor_strong_coinduct_thm,
-      dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms, folded_dtor_map_thms,
-      folded_dtor_set_thmss', dtor_Jrel_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
+    ({bnfs = Jbnfs, dtors = dtors, ctors = ctors, folds = unfolds, recs = corecs,
+      induct = dtor_coinduct_thm, strong_induct = dtor_strong_coinduct_thm,
+      dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
+      map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss',
+      rel_thms = dtor_Jrel_thms, fold_thms = ctor_dtor_unfold_thms,
+      rec_thms = ctor_dtor_corec_thms},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
diff -r be6e703908f4 -r 67757f1d5e71 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Apr 29 09:10:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Apr 29 09:45:14 2013 +0200
@@ -1853,9 +1853,11 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((Ibnfs, dtors, ctors, folds, recs, ctor_induct_thm, ctor_induct_thm, dtor_ctor_thms,
-      ctor_dtor_thms, ctor_inject_thms, folded_ctor_map_thms, folded_ctor_set_thmss',
-      ctor_Irel_thms, ctor_fold_thms, ctor_rec_thms),
+    ({bnfs = Ibnfs, dtors = dtors, ctors = ctors, folds = folds, recs = recs,
+      induct = ctor_induct_thm, strong_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,
+      set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, fold_thms = ctor_fold_thms,
+      rec_thms = ctor_rec_thms},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;