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, induction, ...}: info) rec_eqns = |
233 fun prepare_induct ({descr, inducts = (_, 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 =) (List.concat (map constrs_of rec_eqns)); |
237 val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns); |
238 in |
238 in |
239 induction |
239 induct |
240 |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr))) |
240 |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr)) |
241 |> RuleCases.save induction |
241 |> RuleCases.save induct |
242 end; |
242 end; |
243 |
243 |
244 local |
244 local |
245 |
245 |
246 fun gen_primrec_i note def alt_name eqns_atts thy = |
246 fun gen_primrec_i note def alt_name eqns_atts thy = |