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