use a nicer scheme to indexify names

--- a/src/HOL/BNF/Tools/bnf_fp.ML	Thu Sep 27 18:25:41 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Thu Sep 27 18:39:17 2012 +0200
@@ -257,7 +257,6 @@
 val rel_distinctN = relN ^ "_" ^ distinctN
 val injectN = "inject"
 val rel_injectN = relN ^ "_" ^ injectN
-val relsN = relN ^ "s"
 val selN = "sel"
 val sel_unfoldN = selN ^ "_" ^ unfoldN
 val sel_corecN = selN ^ "_" ^ corecN

--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Thu Sep 27 18:25:41 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Thu Sep 27 18:39:17 2012 +0200
@@ -28,6 +28,19 @@
 open BNF_FP
 open BNF_FP_Sugar_Tactics
 
+(* This function could produce 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;
+    val dups = Library.duplicates (op =) (map fst ps);
+    fun underscore s =
+      let val ss = space_explode Long_Name.separator s in
+        space_implode "_" (drop (length ss - 2) ss)
+      end;
+  in
+    map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
+  end;
+
 val mp_conj = @{thm mp_conj};
 
 val simp_attrs = @{attributes [simp]};
@@ -747,8 +760,7 @@
             `(conj_dests nn) thm
           end;
 
-        (* TODO: Generate nicer names in case of clashes *)
-        val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
+        val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss);
 
         val (fold_thmss, rec_thmss) =
           let
@@ -813,8 +825,8 @@
         val notes =
           [(inductN, map single induct_thms,
             fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
-           (foldN, fold_thmss, K (code_simp_attrs)),
-           (recN, rec_thmss, K (code_simp_attrs)),
+           (foldN, fold_thmss, K code_simp_attrs),
+           (recN, rec_thmss, K code_simp_attrs),
            (simpsN, simp_thmss, K [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map3 (fn b => fn Type (T_name, _) => fn thms =>

--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Sep 27 18:25:41 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Sep 27 18:39:17 2012 +0200
@@ -13,7 +13,7 @@
   val mk_ctr: typ list -> term -> term
   val mk_disc_or_sel: typ list -> term -> term
 
-  val base_name_of_ctr: term -> string
+  val name_of_ctr: term -> string
 
   val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     ((bool * term list) * term) *
@@ -93,11 +93,13 @@
     Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
   end;
 
-fun base_name_of_ctr c =
-  Long_Name.base_name (case head_of c of
-      Const (s, _) => s
-    | Free (s, _) => s
-    | _ => error "Cannot extract name of constructor");
+fun name_of_ctr c =
+  (case head_of c of
+    Const (s, _) => s
+  | Free (s, _) => s
+  | _ => error "Cannot extract name of constructor");
+
+val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;