avoid duplicate case names

--- 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 =