src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML

       val mutual_calls' = tag_list 0 calls
         |> map_filter (try (apsnd (fn Mutual_Rec (_, p) => p)));
       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))))
           nested_calls';