# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 65720ad6dea07f922c979b4397626c77d5703819
# Parent  f9b6af3017fd48e81cb926ea31c48dfdda7317f3
avoid duplicate case names

diff -r f9b6af3017fd -r 65720ad6dea0 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -267,8 +267,6 @@
     #> interpret_fp_sugars plugins fp_sugars
   end;
 
-(* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
-   "x.x_A", "y.A"). *)
 fun quasi_unambiguous_case_names names =
   let
     val ps = map (`Long_Name.base_name) names;
@@ -279,6 +277,7 @@
       end;
   in
     map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
+    |> Name.variant_list []
   end;
 
 fun zipper_map f =