# HG changeset patch
# User blanchet
# Date 1367933518 -7200
# Node ID 826b5f3846e95a250bae2df5221b0a9d4f87e941
# Parent  c2c23ac31973992bd2c8205c19cfee367d283b38
tuning

diff -r c2c23ac31973 -r 826b5f3846e9 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 15:11:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 07 15:31:58 2013 +0200
@@ -39,7 +39,7 @@
     term list list * typ list list * term list list list -> (string -> binding) -> typ list ->
     typ list -> typ list -> term -> term -> Proof.context ->
     (term * term * thm * thm) * local_theory
-  val define_unfold_corec: term list -> int list -> term list list ->
+  val define_unfold_corec: term list -> term list list ->
     (term list list * term list list list list * term list list list list)
       * (typ list * typ list list list * typ list list) ->
     (term list list * term list list list list * term list list list list)
@@ -433,11 +433,13 @@
     map2 mk_terms ctor_folds ctor_recs |> split_list
   end;
 
-fun mk_preds_getterss_join c n cps sum_prod_T cqfss =
-  Term.lambda c (mk_IfN sum_prod_T cps
-    (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
+fun mk_preds_getterss_join c cps sum_prod_T cqfss =
+  let val n = length cqfss in
+    Term.lambda c (mk_IfN sum_prod_T cps
+      (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)))
+  end;
 
-fun mk_coiter_body lthy cs ns cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter =
+fun mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter =
   let
     fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
 
@@ -448,7 +450,7 @@
 
     val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss;
   in
-    Term.list_comb (dtor_coiter, map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss)
+    Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)
   end;
 
 fun mk_unfolds_corecs lthy fpTs As Cs ns mss dtor_unfolds dtor_corecs =
@@ -461,7 +463,7 @@
 
     fun mk_term dtor_coiter ((pfss, cqssss, cfssss), (f_sum_prod_Ts, f_Tsss, _)) =
       fold_rev (fold_rev Term.lambda) pfss
-        (mk_coiter_body lthy cs ns cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter);
+        (mk_coiter_body lthy cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter);
 
     fun mk_terms dtor_unfold dtor_corec =
       (mk_term dtor_unfold unfold_only, mk_term dtor_corec corec_only);
@@ -502,8 +504,8 @@
     ((foldx, recx, fold_def, rec_def), lthy')
   end;
 
-fun define_unfold_corec cs ns cpss unfold_only corec_only mk_binding fpTs As Cs dtor_unfold
-    dtor_corec no_defs_lthy =
+fun define_unfold_corec cs cpss unfold_only corec_only mk_binding fpTs As Cs dtor_unfold dtor_corec
+    no_defs_lthy =
   let
     val nn = length fpTs;
 
@@ -516,8 +518,7 @@
         val binding = mk_binding suf;
         val spec =
           mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
-            mk_coiter_body no_defs_lthy cs ns cpss f_sum_prod_Ts f_Tsss cqssss cfssss
-              dtor_coiter);
+            mk_coiter_body no_defs_lthy cs cpss f_sum_prod_Ts f_Tsss cqssss cfssss dtor_coiter);
       in (binding, spec) end;
 
     val binding_specs =
@@ -1331,7 +1332,7 @@
         (wrap_ctrs
          #> derive_maps_sets_rels
          ##>> (if lfp then define_fold_rec fold_only rec_only
-           else define_unfold_corec cs ns cpss unfold_only corec_only)
+           else define_unfold_corec cs cpss unfold_only corec_only)
              mk_binding fpTs As Cs fp_fold fp_rec
          #> massage_res, lthy')
       end;