# 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;