one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")
authorblanchet
Wed, 05 Jun 2013 13:19:26 +0200
changeset 52303 16d7708aba40
parent 52302 867d5d16158c
child 52304 109bc7d872bc
one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")
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;