equal
deleted
inserted
replaced
92 |
92 |
93 (* order according to constructor names *) |
93 (* order according to constructor names *) |
94 fun cntrs_order ((bn, dt_index), data) = |
94 fun cntrs_order ((bn, dt_index), data) = |
95 let |
95 let |
96 val dt = nth dts dt_index |
96 val dt = nth dts dt_index |
97 val cts = (fn (_, _, _, x) => x) dt |
97 val cts = snd dt |
98 val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts |
98 val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts |
99 in |
99 in |
100 (bn, (bn, dt_index, order (op=) ct_names data)) |
100 (bn, (bn, dt_index, order (op=) ct_names data)) |
101 end |
101 end |
102 in |
102 in |