71 val auto_minimize_max_time = |
71 val auto_minimize_max_time = |
72 Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} |
72 Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} |
73 (K 5.0) |
73 (K 5.0) |
74 |
74 |
75 fun adjust_reconstructor_params override_params |
75 fun adjust_reconstructor_params override_params |
76 ({debug, verbose, overlord, blocking, provers, type_enc, sound, |
76 ({debug, verbose, overlord, blocking, provers, type_enc, strict, |
77 lam_trans, relevance_thresholds, max_relevant, max_mono_iters, |
77 lam_trans, relevance_thresholds, max_relevant, max_mono_iters, |
78 max_new_mono_instances, isar_proof, isar_shrink_factor, slice, |
78 max_new_mono_instances, isar_proof, isar_shrink_factor, slice, |
79 minimize, timeout, preplay_timeout, expect} : params) = |
79 minimize, timeout, preplay_timeout, expect} : params) = |
80 let |
80 let |
81 fun lookup_override name default_value = |
81 fun lookup_override name default_value = |
86 here. *) |
86 here. *) |
87 val type_enc = lookup_override "type_enc" type_enc |
87 val type_enc = lookup_override "type_enc" type_enc |
88 val lam_trans = lookup_override "lam_trans" lam_trans |
88 val lam_trans = lookup_override "lam_trans" lam_trans |
89 in |
89 in |
90 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
90 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
91 provers = provers, type_enc = type_enc, sound = sound, |
91 provers = provers, type_enc = type_enc, strict = strict, |
92 lam_trans = lam_trans, max_relevant = max_relevant, |
92 lam_trans = lam_trans, max_relevant = max_relevant, |
93 relevance_thresholds = relevance_thresholds, |
93 relevance_thresholds = relevance_thresholds, |
94 max_mono_iters = max_mono_iters, |
94 max_mono_iters = max_mono_iters, |
95 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
95 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
96 isar_shrink_factor = isar_shrink_factor, slice = slice, |
96 isar_shrink_factor = isar_shrink_factor, slice = slice, |