diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Aug 27 12:57:55 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