# HG changeset patch
# User blanchet
# Date 1347291159 -7200
# Node ID edc322ac527932d818c0132b0219443d91da3996
# Parent  4b11240d80bfe557167d1907356226c07cab3850
busted -- let's use more neutral names

diff -r 4b11240d80bf -r edc322ac5279 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 14:52:22 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:32:39 2012 +0200
@@ -245,8 +245,8 @@
           val p_Tss =
             map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
 
-          fun popescu_zip [] [fs] = fs
-            | popescu_zip (p :: ps) (fs :: fss) = p :: fs @ popescu_zip ps fss;
+          fun zip_preds_getters [] [fs] = fs
+            | zip_preds_getters (p :: ps) (fs :: fss) = p :: fs @ zip_preds_getters ps fss;
 
           fun mk_types fun_Ts =
             let
@@ -254,7 +254,7 @@
               val f_prod_Tss = map2 dest_sumTN ns f_sum_prod_Ts;
               val f_Tsss =
                 map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
-              val pf_Tss = map2 popescu_zip p_Tss f_Tsss
+              val pf_Tss = map2 zip_preds_getters p_Tss f_Tsss
             in (f_sum_prod_Ts, f_prod_Tss, f_Tsss, pf_Tss) end;
 
           val (g_sum_prod_Ts, g_prod_Tss, g_Tsss, pg_Tss) = mk_types fp_iter_fun_Ts;
@@ -273,7 +273,7 @@
 
           fun mk_terms fsss =
             let
-              val pfss = map2 popescu_zip pss fsss;
+              val pfss = map2 zip_preds_getters pss fsss;
               val cfsss = map2 (fn c => map (map (fn f => f $ c))) cs fsss
             in (pfss, cfsss) end;
         in
@@ -409,14 +409,14 @@
 
                 val binder = Binding.suffix_name ("_" ^ suf) b;
 
-                fun mk_popescu_join c n cps sum_prod_T prod_Ts cfss =
+                fun mk_preds_getters_join c n cps sum_prod_T prod_Ts cfss =
                   Term.lambda c (mk_IfN sum_prod_T cps
                     (map2 (mk_InN prod_Ts) (map HOLogic.mk_tuple cfss) (1 upto n)));
 
                 val spec =
                   mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
                     Term.list_comb (fp_iter_like,
-                      map6 mk_popescu_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss));
+                      map6 mk_preds_getters_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss));
               in (binder, spec) end;
 
             val coiter_likes =