# HG changeset patch
# User bulwahn
# Date 1279728711 -7200
# Node ID 8f99e388086438fd05c10d6c8051f60a6ab2d8ba
# Parent  555287ba8d8d5d829e1bdb6e40926e108e9319ea
correcting merging of default_types

diff -r 555287ba8d8d -r 8f99e3880864 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/quickcheck.ML	Wed Jul 21 18:11:51 2010 +0200
@@ -82,7 +82,7 @@
   Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
                 no_assms = no_assms2, report = report2, quiet = quiet2 }) =
   make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
-    ((default_type1 @ default_type2, no_assms1 orelse no_assms2),
+    ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
     (report1 orelse report2, quiet1 orelse quiet2)));
 
 structure Data = Theory_Data