80 fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1, |
80 fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1, |
81 no_assms = no_assms1, report = report1, quiet = quiet1 }, |
81 no_assms = no_assms1, report = report1, quiet = quiet1 }, |
82 Test_Params { size = size2, iterations = iterations2, default_type = default_type2, |
82 Test_Params { size = size2, iterations = iterations2, default_type = default_type2, |
83 no_assms = no_assms2, report = report2, quiet = quiet2 }) = |
83 no_assms = no_assms2, report = report2, quiet = quiet2 }) = |
84 make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), |
84 make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), |
85 ((default_type1 @ default_type2, no_assms1 orelse no_assms2), |
85 ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2), |
86 (report1 orelse report2, quiet1 orelse quiet2))); |
86 (report1 orelse report2, quiet1 orelse quiet2))); |
87 |
87 |
88 structure Data = Theory_Data |
88 structure Data = Theory_Data |
89 ( |
89 ( |
90 type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list |
90 type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list |