tuning
authorblanchet
Fri Jun 07 09:30:13 2013 +0200 (2013-06-07)
changeset 52334705bc4f5fc70
parent 52330 8ce7fba90bb3
child 52335 0e3f949792ca
tuning
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 09:28:59 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 09:30:13 2013 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    val flat_rec: 'a list list -> 'a list
     1.5    val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
     1.6    val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
     1.7 -  val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
     1.8 +  val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
     1.9      int list list -> term list list -> Proof.context ->
    1.10      (term list list
    1.11       * (typ list list * typ list list list list * term list list
    1.12 @@ -355,7 +355,7 @@
    1.13      ((cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
    1.14    end;
    1.15  
    1.16 -fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy =
    1.17 +fun mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy =
    1.18    let
    1.19      val thy = Proof_Context.theory_of lthy;
    1.20  
    1.21 @@ -369,7 +369,7 @@
    1.22        else
    1.23          mk_coiters_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (pair NONE o SOME)
    1.24    in
    1.25 -    ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy')
    1.26 +    ((transpose xtor_co_iterss', iters_args_types, coiters_args_types), lthy')
    1.27    end;
    1.28  
    1.29  fun mk_map live Ts Us t =
    1.30 @@ -1099,9 +1099,8 @@
    1.31      val kss = map (fn n => 1 upto n) ns;
    1.32      val mss = map (map length) ctr_Tsss;
    1.33  
    1.34 -    val ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy) =
    1.35 -      mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
    1.36 -    val xtor_co_iterss = transpose xtor_co_iterss';
    1.37 +    val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy) =
    1.38 +      mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
    1.39  
    1.40      fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
    1.41                xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),