1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 14:52:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:32:39 2012 +0200
     1.3 @@ -245,8 +245,8 @@
     1.4            val p_Tss =
     1.5              map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
     1.6  
     1.7 -          fun popescu_zip [] [fs] = fs
     1.8 -            | popescu_zip (p :: ps) (fs :: fss) = p :: fs @ popescu_zip ps fss;
     1.9 +          fun zip_preds_getters [] [fs] = fs
    1.10 +            | zip_preds_getters (p :: ps) (fs :: fss) = p :: fs @ zip_preds_getters ps fss;
    1.11  
    1.12            fun mk_types fun_Ts =
    1.13              let
    1.14 @@ -254,7 +254,7 @@
    1.15                val f_prod_Tss = map2 dest_sumTN ns f_sum_prod_Ts;
    1.16                val f_Tsss =
    1.17                  map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
    1.18 -              val pf_Tss = map2 popescu_zip p_Tss f_Tsss
    1.19 +              val pf_Tss = map2 zip_preds_getters p_Tss f_Tsss
    1.20              in (f_sum_prod_Ts, f_prod_Tss, f_Tsss, pf_Tss) end;
    1.21  
    1.22            val (g_sum_prod_Ts, g_prod_Tss, g_Tsss, pg_Tss) = mk_types fp_iter_fun_Ts;
    1.23 @@ -273,7 +273,7 @@
    1.24  
    1.25            fun mk_terms fsss =
    1.26              let
    1.27 -              val pfss = map2 popescu_zip pss fsss;
    1.28 +              val pfss = map2 zip_preds_getters pss fsss;
    1.29                val cfsss = map2 (fn c => map (map (fn f => f $ c))) cs fsss
    1.30              in (pfss, cfsss) end;
    1.31          in
    1.32 @@ -409,14 +409,14 @@
    1.33  
    1.34                  val binder = Binding.suffix_name ("_" ^ suf) b;
    1.35  
    1.36 -                fun mk_popescu_join c n cps sum_prod_T prod_Ts cfss =
    1.37 +                fun mk_preds_getters_join c n cps sum_prod_T prod_Ts cfss =
    1.38                    Term.lambda c (mk_IfN sum_prod_T cps
    1.39                      (map2 (mk_InN prod_Ts) (map HOLogic.mk_tuple cfss) (1 upto n)));
    1.40  
    1.41                  val spec =
    1.42                    mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
    1.43                      Term.list_comb (fp_iter_like,
    1.44 -                      map6 mk_popescu_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss));
    1.45 +                      map6 mk_preds_getters_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss));
    1.46                in (binder, spec) end;
    1.47  
    1.48              val coiter_likes =