| changeset 41493 | f05976d69141 |
| parent 41114 | f9ae7c2abf7e |
| child 42361 | 23f352990944 |
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Jan 10 16:07:16 2011 +0100 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Jan 10 16:45:28 2011 +0100 @@ -68,7 +68,7 @@ type T = multiset_setup option val empty = NONE val extend = I; - fun merge (v1, v2) = if is_some v1 then v1 else v2 + val merge = merge_options ) val multiset_setup = Multiset_Setup.put o SOME