prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)

--- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Mon Dec 23 09:21:38 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Mon Dec 23 15:30:31 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))))