equal
deleted
inserted
replaced
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 = |
247 let |
247 let |
248 val (eqns, atts) = split_list eqns_atts; |
248 val (eqns, atts) = split_list eqns_atts; |
249 val dt_info = Datatype.get_all thy; |
249 val dt_info = Datatype_Data.get_all thy; |
250 val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ; |
250 val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ; |
251 val tnames = distinct (op =) (map (#1 o snd) rec_eqns); |
251 val tnames = distinct (op =) (map (#1 o snd) rec_eqns); |
252 val dts = find_dts dt_info tnames tnames; |
252 val dts = find_dts dt_info tnames tnames; |
253 val main_fns = |
253 val main_fns = |
254 map (fn (tname, {index, ...}) => |
254 map (fn (tname, {index, ...}) => |