src/HOL/Tools/Function/scnp_reconstruct.ML
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