72 ( |
72 ( |
73 type T = {splits: thm list, |
73 type T = {splits: thm list, |
74 inj_consts: (string * typ) list, |
74 inj_consts: (string * typ) list, |
75 discrete: string list}; |
75 discrete: string list}; |
76 val empty = {splits = [], inj_consts = [], discrete = []}; |
76 val empty = {splits = [], inj_consts = [], discrete = []}; |
77 val extend = I; |
|
78 fun merge |
77 fun merge |
79 ({splits = splits1, inj_consts = inj_consts1, discrete = discrete1}, |
78 ({splits = splits1, inj_consts = inj_consts1, discrete = discrete1}, |
80 {splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T = |
79 {splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T = |
81 {splits = Thm.merge_thms (splits1, splits2), |
80 {splits = Thm.merge_thms (splits1, splits2), |
82 inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), |
81 inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), |