changeset 38761 | b32975d3db3e |
parent 36521 | 73ed9f18fdd3 |
child 39923 | 0e1bd289c8ea |
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Aug 26 16:56:45 2010 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Aug 26 17:01:12 2010 +0200 @@ -68,7 +68,7 @@ type T = multiset_setup option val empty = NONE val extend = I; - fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *) + fun merge (v1, v2) = if is_some v1 then v1 else v2 ) val multiset_setup = Multiset_Setup.put o SOME