# HG changeset patch
# User blanchet
# Date 1370431166 -7200
# Node ID 16d7708aba4022e7f457936a5192db71e1a79622
# Parent  867d5d16158cfd469e9e546cfd8ce6fbb7d96475
one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")

diff -r 867d5d16158c -r 16d7708aba40 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 13:13:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 13:19:26 2013 +0200
@@ -681,8 +681,8 @@
 
         fun unzip_iters tick fiters (x as Free (_, T)) =
           map (fn U => if U = T then x else
-            build_map lthy (indexify fst fpTs (fn kk => fn TU =>
-              nth fiters kk |> maybe_tick TU (nth us kk))) (T, U) $ x);
+            build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
+              (fn kk => fn TU => nth fiters kk |> maybe_tick TU (nth us kk))) (T, U) $ x);
 
         val gxsss = map2 (map2 (flat_rec oo map2 (unzip_iters false gfolds))) xsss y_Tssss;
         val hxsss = map2 (map2 (flat_rec oo map2 (unzip_iters true hrecs))) xsss z_Tssss;