equal
deleted
inserted
replaced
36 mk_selectors T binder_Ts sels #>> pair ctr |
36 mk_selectors T binder_Ts sels #>> pair ctr |
37 end |
37 end |
38 |
38 |
39 val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0 |
39 val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0 |
40 in |
40 in |
41 Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt |
41 @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt |
42 |>> (pair T #> single) |
42 |>> (pair T #> single) |
43 end |
43 end |
44 |
44 |
45 |
45 |
46 (* typedef declarations *) |
46 (* typedef declarations *) |