equal
deleted
inserted
replaced
224 fun find_dts (dt_info : info Symtab.table) _ [] = [] |
224 fun find_dts (dt_info : info Symtab.table) _ [] = [] |
225 | find_dts dt_info tnames' (tname::tnames) = |
225 | find_dts dt_info tnames' (tname::tnames) = |
226 (case Symtab.lookup dt_info tname of |
226 (case Symtab.lookup dt_info tname of |
227 NONE => primrec_err (quote tname ^ " is not a datatype") |
227 NONE => primrec_err (quote tname ^ " is not a datatype") |
228 | SOME dt => |
228 | SOME dt => |
229 if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then |
229 if subset (op =) (tnames', 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, induct, ...}: info) rec_eqns = |
233 fun prepare_induct ({descr, induct, ...}: info) rec_eqns = |
234 let |
234 let |
263 fold_rev (process_fun thy descr rec_eqns) main_fns ([], []); |
263 fold_rev (process_fun thy descr rec_eqns) main_fns ([], []); |
264 val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []); |
264 val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []); |
265 val defs' = map (make_def thy fs) defs; |
265 val defs' = map (make_def thy fs) defs; |
266 val nameTs1 = map snd fnameTs; |
266 val nameTs1 = map snd fnameTs; |
267 val nameTs2 = map fst rec_eqns; |
267 val nameTs2 = map fst rec_eqns; |
268 val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then () |
268 val _ = if eq_set (op =) (nameTs1, nameTs2) then () |
269 else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^ |
269 else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^ |
270 "\nare not mutually recursive"); |
270 "\nare not mutually recursive"); |
271 val primrec_name = |
271 val primrec_name = |
272 if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name; |
272 if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name; |
273 val (defs_thms', thy') = |
273 val (defs_thms', thy') = |