src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 58685 6a75a4c24339
parent 58675 69571f0a93df
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 15 17:15:11 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 15 17:18:08 2014 +0200
     1.3 @@ -128,10 +128,10 @@
     1.4     split_sel_asms: thm list,
     1.5     case_eq_ifs: thm list};
     1.6  
     1.7 -fun morph_ctr_sugar phi {kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     1.8 +fun morph_ctr_sugar phi ({kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     1.9      case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
    1.10      sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
    1.11 -    split_sel_asms, case_eq_ifs} =
    1.12 +    split_sel_asms, case_eq_ifs} : ctr_sugar) =
    1.13    {kind = kind,
    1.14     T = Morphism.typ phi T,
    1.15     ctrs = map (Morphism.term phi) ctrs,