86 val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ |
86 val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ |
87 (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") |
87 (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") |
88 |
88 |
89 val facts = facts |> maps (fn (n, ths) => map (pair n) ths) |
89 val facts = facts |> maps (fn (n, ths) => map (pair n) ths) |
90 val params = |
90 val params = |
91 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, |
91 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, |
92 provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
92 type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
93 uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, |
93 uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, |
94 max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), |
94 max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), |
95 max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, |
95 max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, |
96 isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, |
96 isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, |
97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |