# HG changeset patch
# User blanchet
# Date 1382633459 -7200
# Node ID 334a29265b2df1bf51fe1207239aaaf81c25945b
# Parent  064f88a410962c2983397a7edd4a90d4b8bd5cc5
tuning

diff -r 064f88a41096 -r 334a29265b2d src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 24 18:37:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Oct 24 18:50:59 2013 +0200
@@ -231,7 +231,7 @@
       val args = replicate n_args ("", dummyT)
         |> Term.rename_wrt_term t
         |> map Free
-        |> fold (fn (ctr_arg_idx, (arg_idx, T)) =>
+        |> fold (fn (ctr_arg_idx, (arg_idx, _)) =>
             nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
           no_calls'
         |> fold (fn (ctr_arg_idx, (arg_idx, T)) =>