generate unique names
authorblanchet
Fri Feb 14 15:14:35 2014 +0100 (2014-02-14)
changeset 55481a8b83356e869
parent 55480 59cc4a8bc28a
child 55482 61ffc2339a8c
generate unique names
src/HOL/Tools/BNF/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Feb 14 15:03:24 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Feb 14 15:14:35 2014 +0100
     1.3 @@ -105,7 +105,7 @@
     1.4      val Ts = map fst Tkkssss;
     1.5      val callssss = map (map (map (map Bound)) o snd) Tkkssss;
     1.6  
     1.7 -    val b_names = map base_name_of_typ Ts;
     1.8 +    val b_names = Name.variant_list [] (map base_name_of_typ Ts);
     1.9      val compat_b_names = map (prefix compatN) b_names;
    1.10      val compat_bs = map Binding.name compat_b_names;
    1.11      val common_name = compatN ^ mk_common_name b_names;