correcting merging of default_types
authorbulwahn
Wed, 21 Jul 2010 18:11:51 +0200
changeset 37911 8f99e3880864
parent 37910 555287ba8d8d
child 37912 247042107f93
correcting merging of default_types
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