eliminated dead argument
authorblanchet
Wed, 05 Jun 2013 13:22:44 +0200
changeset 52304 109bc7d872bc
parent 52303 16d7708aba40
child 52305 3f7b92017d71
eliminated dead argument
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;