40 "") |
40 "") |
41 end |
41 end |
42 |
42 |
43 fun print silent f = if silent then () else Output.urgent_message (f ()) |
43 fun print silent f = if silent then () else Output.urgent_message (f ()) |
44 |
44 |
45 fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof, |
45 fun test_facts ({debug, verbose, overlord, provers, monomorphize_limit, |
46 isar_shrink_factor, ...} : params) |
46 type_sys, isar_proof, isar_shrink_factor, ...} : params) |
47 explicit_apply_opt silent (prover : prover) timeout i n state facts = |
47 explicit_apply_opt silent (prover : prover) timeout i n state facts = |
48 let |
48 let |
49 val thy = Proof.theory_of state |
49 val thy = Proof.theory_of state |
50 val _ = |
50 val _ = |
51 print silent (fn () => |
51 print silent (fn () => |
63 end |
63 end |
64 val params = |
64 val params = |
65 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
65 {debug = debug, verbose = verbose, overlord = overlord, blocking = true, |
66 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
66 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
67 relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
67 relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
|
68 monomorphize = false, monomorphize_limit = monomorphize_limit, |
68 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
69 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
69 timeout = timeout, expect = ""} |
70 timeout = timeout, expect = ""} |
70 val facts = |
71 val facts = |
71 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
72 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
72 val problem = |
73 val problem = |