# HG changeset patch
# User blanchet
# Date 1370590213 -7200
# Node ID 705bc4f5fc7083c75d332f728c67a71d683085af
# Parent  8ce7fba90bb39beae0b5be8a4ebfbe158b75ef2a
tuning

diff -r 8ce7fba90bb3 -r 705bc4f5fc70 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 09:28:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 09:30:13 2013 +0200
@@ -31,7 +31,7 @@
   val flat_rec: 'a list list -> 'a list
   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
-  val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
+  val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
     int list list -> term list list -> Proof.context ->
     (term list list
      * (typ list list * typ list list list list * term list list
@@ -355,7 +355,7 @@
     ((cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
   end;
 
-fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy =
+fun mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
@@ -369,7 +369,7 @@
       else
         mk_coiters_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (pair NONE o SOME)
   in
-    ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy')
+    ((transpose xtor_co_iterss', iters_args_types, coiters_args_types), lthy')
   end;
 
 fun mk_map live Ts Us t =
@@ -1099,9 +1099,8 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy) =
-      mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
-    val xtor_co_iterss = transpose xtor_co_iterss';
+    val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy) =
+      mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
 
     fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
               xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),