more liberal merging of BNFs and constructor sugar
* * *
make sure that the cache doesn't produce 'DUP's

--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -12,7 +12,6 @@
   type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
 
   val morph_bnf: morphism -> bnf -> bnf
-  val eq_bnf: bnf * bnf -> bool
   val bnf_of: Proof.context -> string -> bnf option
   val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
 
@@ -452,16 +451,12 @@
     wits = List.map (morph_witness phi) wits,
     rel = Morphism.term phi rel};
 
-fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
-  BNF {T = T2, live = live2, dead = dead2, ...}) =
-  Type.could_unify (T1, T2) andalso live1 = live2 andalso dead1 = dead2;
-
 structure Data = Generic_Data
 (
   type T = bnf Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-  val merge = Symtab.merge eq_bnf;
+  fun merge data : T = Symtab.merge (K true) data;
 );
 
 fun bnf_of ctxt =

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -25,7 +25,6 @@
      sel_co_iterssss: thm list list list list};
 
   val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
-  val eq_fp_sugar: fp_sugar * fp_sugar -> bool
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
   val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
   val fp_sugar_of: Proof.context -> string -> fp_sugar option
@@ -136,10 +135,6 @@
 
 fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
 
-fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
-    {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
-  T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
-
 fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
     ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss}
     : fp_sugar) =
@@ -163,7 +158,7 @@
   type T = fp_sugar Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-  val merge = Symtab.merge eq_fp_sugar;
+  fun merge data : T = Symtab.merge (K true) data;
 );
 
 fun fp_sugar_of ctxt =

--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -97,12 +97,12 @@
     val pre_bnfss = map #pre_bnfs fp_sugars;
     val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
     val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
-    val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
+    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
 
     val rels =
       let
         fun find_rel T As Bs = fp_nesty_bnfss
-          |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
+          |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
           |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
           |> Option.map (fn bnf =>
             let val live = live_of_bnf bnf;

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -43,7 +43,7 @@
   type T = n2m_sugar Typtab.table;
   val empty = Typtab.empty;
   val extend = I;
-  fun merge data : T = Typtab.merge (eq_fst (eq_list eq_fp_sugar)) data;
+  fun merge data : T = Typtab.merge (K true) data;
 );
 
 fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -30,7 +30,6 @@
      rel_xtor_co_induct_thm: thm}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
-  val eq_fp_result: fp_result * fp_result -> bool
   val un_fold_of: 'a list -> 'a
   val co_rec_of: 'a list -> 'a
 
@@ -239,9 +238,6 @@
    xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
    rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
 
-fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
-  eq_list eq_bnf (bnfs1, bnfs2);
-
 fun un_fold_of [f, _] = f;
 fun co_rec_of [_, r] = r;
 

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -96,10 +96,6 @@
    sel_split_asms: thm list,
    case_eq_ifs: thm list};
 
-fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
-    {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
-  ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
-
 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
     disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
@@ -137,7 +133,7 @@
   type T = ctr_sugar Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-  val merge = Symtab.merge eq_ctr_sugar;
+  fun merge data : T = Symtab.merge (K true) data;
 );
 
 fun ctr_sugar_of ctxt =