equal
deleted
inserted
replaced
228 | SOME dt => |
228 | SOME dt => |
229 if tnames' subset (map (#1 o snd) (#descr dt)) then |
229 if tnames' subset (map (#1 o snd) (#descr dt)) then |
230 (tname, dt)::(find_dts dt_info tnames' tnames) |
230 (tname, dt)::(find_dts dt_info tnames' tnames) |
231 else find_dts dt_info tnames' tnames); |
231 else find_dts dt_info tnames' tnames); |
232 |
232 |
233 fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns = |
233 fun prepare_induct ({descr, induct, ...}: info) rec_eqns = |
234 let |
234 let |
235 fun constrs_of (_, (_, _, cs)) = |
235 fun constrs_of (_, (_, _, cs)) = |
236 map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs; |
236 map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs; |
237 val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns); |
237 val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns); |
238 in |
238 in |