equal
deleted
inserted
replaced
66 structure Multiset_Setup = Theory_Data |
66 structure Multiset_Setup = Theory_Data |
67 ( |
67 ( |
68 type T = multiset_setup option |
68 type T = multiset_setup option |
69 val empty = NONE |
69 val empty = NONE |
70 val extend = I; |
70 val extend = I; |
71 fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *) |
71 fun merge (v1, v2) = if is_some v1 then v1 else v2 |
72 ) |
72 ) |
73 |
73 |
74 val multiset_setup = Multiset_Setup.put o SOME |
74 val multiset_setup = Multiset_Setup.put o SOME |
75 |
75 |
76 fun undef _ = error "undef" |
76 fun undef _ = error "undef" |