equal
deleted
inserted
replaced
523 in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end; |
523 in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end; |
524 |
524 |
525 |
525 |
526 (* registering code types in code generator *) |
526 (* registering code types in code generator *) |
527 |
527 |
528 val codetype_hook = |
528 fun codetype_hook x = |
529 fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec)); |
529 fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec)) x; |
530 |
530 |
531 |
531 |
532 (* instrumentalizing the sort algebra *) |
532 (* instrumentalizing the sort algebra *) |
533 |
533 |
534 (*fun assume_arities_of_sort thy arities ty_sort = |
534 (*fun assume_arities_of_sort thy arities ty_sort = |