--- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML Mon Dec 23 16:16:36 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML Mon Dec 23 16:59:56 2013 +0100
@@ -370,14 +370,17 @@
val nested_calls' = tag_list 0 calls
|> map_filter (try (apsnd (fn Nested_Rec p => p)));
+ fun ensure_unique frees t =
+ if member (op =) frees t then Free (the_single (Term.variant_frees t [dest_Free t])) else t;
+
val args = replicate n_args ("", dummyT)
|> Term.rename_wrt_term t
|> map Free
|> 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)) =>
- nth_map arg_idx (K (retype_free T (nth ctr_args ctr_arg_idx))))
+ |> fold (fn (ctr_arg_idx, (arg_idx, T)) => fn xs =>
+ nth_map arg_idx (K (ensure_unique xs (retype_free T (nth ctr_args ctr_arg_idx)))) xs)
mutual_calls'
|> fold (fn (ctr_arg_idx, (arg_idx, T)) =>
nth_map arg_idx (K (retype_free T (nth ctr_args ctr_arg_idx))))