author | blanchet |
Thu, 24 Oct 2013 18:50:59 +0200 | |
changeset 54201 | 334a29265b2d |
parent 54200 | 064f88a41096 |
child 54202 | 0a06b51ffa56 |
--- 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)) =>