# HG changeset patch
# User blanchet
# Date 1392387275 -3600
# Node ID a8b83356e869fc1b2ae852279eeb98433f325192
# Parent  59cc4a8bc28a1ed059e18ff2c6029d16fdaa3814
generate unique names

diff -r 59cc4a8bc28a -r a8b83356e869 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Feb 14 15:03:24 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Feb 14 15:14:35 2014 +0100
@@ -105,7 +105,7 @@
     val Ts = map fst Tkkssss;
     val callssss = map (map (map (map Bound)) o snd) Tkkssss;
 
-    val b_names = map base_name_of_typ Ts;
+    val b_names = Name.variant_list [] (map base_name_of_typ Ts);
     val compat_b_names = map (prefix compatN) b_names;
     val compat_bs = map Binding.name compat_b_names;
     val common_name = compatN ^ mk_common_name b_names;