equal
deleted
inserted
replaced
541 let |
541 let |
542 val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos; |
542 val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos; |
543 in try (Code.add_datatype cs) thy |> the_default thy end; |
543 in try (Code.add_datatype cs) thy |> the_default thy end; |
544 |
544 |
545 val codetype_hook = |
545 val codetype_hook = |
546 fold (fn (dtco, (_, spec)) => add_datatype_spec (dtco, spec)); |
546 fold (fn (dtco, (_ : bool, spec)) => add_datatype_spec (dtco, spec)); |
547 |
547 |
548 |
548 |
549 (* instrumentalizing the sort algebra *) |
549 (* instrumentalizing the sort algebra *) |
550 |
550 |
551 fun get_codetypes_arities thy tycos sort = |
551 fun get_codetypes_arities thy tycos sort = |