# HG changeset patch
# User blanchet
# Date 1348646459 -7200
# Node ID 33cf557c7849833dcb4757c96072fc0ba84c6755
# Parent  d5e342ffe91e919ba9133e91c84baffc8bda3d66
name tuning

diff -r d5e342ffe91e -r 33cf557c7849 src/HOL/BNF/Tools/bnf_fp_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -319,11 +319,11 @@
 
           val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
 
-          fun zip_predss_getterss qss fss = maps (op @) (qss ~~ fss);
+          fun flat_predss_getterss qss fss = maps (op @) (qss ~~ fss);
 
-          fun zip_preds_predsss_gettersss [] [qss] [fss] = zip_predss_getterss qss fss
-            | zip_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
-              p :: zip_predss_getterss qss fss @ zip_preds_predsss_gettersss ps qsss fsss;
+          fun flat_preds_predsss_gettersss [] [qss] [fss] = flat_predss_getterss qss fss
+            | flat_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
+              p :: flat_predss_getterss qss fss @ flat_preds_predsss_gettersss ps qsss fsss;
 
           fun mk_types maybe_dest_sumT fun_Ts =
             let
@@ -334,7 +334,7 @@
                   Cs mss' f_prod_Tss;
               val q_Tssss =
                 map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss;
-              val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
+              val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
             in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end;
 
           val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_fold_fun_Ts;
@@ -368,7 +368,7 @@
 
           fun mk_terms qssss fssss =
             let
-              val pfss = map3 zip_preds_predsss_gettersss pss qssss fssss;
+              val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss;
               val cqssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs qssss;
               val cfssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs fssss;
               val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss;
@@ -968,13 +968,13 @@
         val sel_unfold_thmss = mk_sel_corec_like_thms unfold_thmss;
         val sel_corec_thmss = mk_sel_corec_like_thms corec_thmss;
 
-        fun zip_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
+        fun flat_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
           corec_likes @ disc_corec_likes @ sel_corec_likes;
 
         val simp_thmss =
           mk_simp_thmss wrap_ress
-            (map3 zip_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
-            (map3 zip_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
+            (map3 flat_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
+            (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
 
         val anonymous_notes =
           [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]