equal
deleted
inserted
replaced
78 val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls |
78 val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls |
79 val (contconst_decls, normal_decls) = List.partition is_contconst decls |
79 val (contconst_decls, normal_decls) = List.partition is_contconst decls |
80 val transformed_decls = map (transform thy) contconst_decls |
80 val transformed_decls = map (transform thy) contconst_decls |
81 in |
81 in |
82 thy |
82 thy |
83 |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |
83 |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) |
84 |> Sign.add_trrules (maps #3 transformed_decls) |
84 |> Sign.add_trrules (maps #3 transformed_decls) |
85 end |
85 end |
86 |
86 |
87 in |
87 in |
88 |
88 |