equal
deleted
inserted
replaced
132 |
132 |
133 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |
133 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |
134 |> map (map snd) |
134 |> map (map snd) |
135 |
135 |
136 |
136 |
137 val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding |
137 val bnds' = bnds @ replicate (length spliteqs - length bnds) Binding.empty_atts |
138 |
138 |
139 (* using theorem names for case name currently disabled *) |
139 (* using theorem names for case name currently disabled *) |
140 val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) |
140 val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) |
141 (bnds' ~~ spliteqs) |> flat |
141 (bnds' ~~ spliteqs) |> flat |
142 in |
142 in |