src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55394 d5ebe055b599
parent 55356 3ea8ace6bc8a
child 55407 81f7e60755c3
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -96,10 +96,6 @@
     1.4     sel_split_asms: thm list,
     1.5     case_eq_ifs: thm list};
     1.6  
     1.7 -fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
     1.8 -    {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
     1.9 -  ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
    1.10 -
    1.11  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    1.12      case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    1.13      disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
    1.14 @@ -137,7 +133,7 @@
    1.15    type T = ctr_sugar Symtab.table;
    1.16    val empty = Symtab.empty;
    1.17    val extend = I;
    1.18 -  val merge = Symtab.merge eq_ctr_sugar;
    1.19 +  fun merge data : T = Symtab.merge (K true) data;
    1.20  );
    1.21  
    1.22  fun ctr_sugar_of ctxt =