src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

           val mss' =  map (fn [0] => [1] | ms => ms) mss;
 
           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
               val f_sum_prod_Ts = map range_type fun_Ts;
               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;
           val (h_sum_prod_Ts, h_prod_Tss, h_Tsss, ph_Tss) = mk_types fp_rec_fun_Ts;
 

 
           val cpss = map2 (fn c => map (fn p => p $ c)) cs pss;
 
           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
           ((([], [], []), ([], [], [])),
            ([z], cs, cpss, p_Tss, (mk_terms gsss, g_sum_prod_Ts, g_prod_Tss, pg_Tss),

               let
                 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
 
                 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 =
               [(coiterN, fp_iter, coiter_only),
                (corecN, fp_rec, corec_only)];