# HG changeset patch
# User blanchet
# Date 1370431364 -7200
# Node ID 109bc7d872bc6532a20c3dec1d8ca5ef05fc5f62
# Parent  16d7708aba4022e7f457936a5192db71e1a79622
eliminated dead argument

diff -r 16d7708aba40 -r 109bc7d872bc src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 13:19:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 13:22:44 2013 +0200
@@ -679,13 +679,13 @@
           else
             f;
 
-        fun unzip_iters tick fiters (x as Free (_, T)) =
+        fun unzip_iters fiters (x as Free (_, T)) =
           map (fn U => if U = T then x else
             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;
+        val gxsss = map2 (map2 (flat_rec oo map2 (unzip_iters gfolds))) xsss y_Tssss;
+        val hxsss = map2 (map2 (flat_rec oo map2 (unzip_iters hrecs))) xsss z_Tssss;
 
         val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
         val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;