77 inj_consts: (string * typ) list, |
77 inj_consts: (string * typ) list, |
78 discrete: string list}; |
78 discrete: string list}; |
79 val empty = {splits = [], inj_consts = [], discrete = []}; |
79 val empty = {splits = [], inj_consts = [], discrete = []}; |
80 val extend = I; |
80 val extend = I; |
81 fun merge |
81 fun merge |
82 ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1}, |
82 ({splits = splits1, inj_consts = inj_consts1, discrete = discrete1}, |
83 {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T = |
83 {splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T = |
84 {splits = Thm.merge_thms (splits1, splits2), |
84 {splits = Thm.merge_thms (splits1, splits2), |
85 inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), |
85 inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), |
86 discrete = Library.merge (op =) (discrete1, discrete2)}; |
86 discrete = Library.merge (op =) (discrete1, discrete2)}; |
87 ); |
87 ); |
88 |
88 |