equal
deleted
inserted
replaced
623 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
623 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
624 in |
624 in |
625 map_index (prep_typ binds) annos |
625 map_index (prep_typ binds) annos |
626 end |
626 end |
627 |
627 |
628 in |
628 val result = map (map (map (map (fn (a, b, c) => |
629 map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) |
629 (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) |
630 (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) |
630 (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) |
|
631 |
|
632 val _ = warning (@{make_string} result) |
|
633 |
|
634 in |
|
635 result |
631 end |
636 end |
632 *} |
637 *} |
633 |
638 |
634 ML {* |
639 ML {* |
635 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
640 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |