53 provers = provers, full_types = full_types, |
53 provers = provers, full_types = full_types, |
54 explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), |
54 explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), |
55 max_relevant = NONE, isar_proof = isar_proof, |
55 max_relevant = NONE, isar_proof = isar_proof, |
56 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
56 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
57 val facts = |
57 val facts = |
58 facts |> maps (fn (n, ths) => ths |> map (Untranslated o pair n)) |
58 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
59 val {goal, ...} = Proof.goal state |
59 val {goal, ...} = Proof.goal state |
60 val problem = |
60 val problem = |
61 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
61 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
62 facts = facts} |
62 facts = facts} |
63 val result as {outcome, used_facts, ...} = prover params (K "") problem |
63 val result as {outcome, used_facts, ...} = prover params (K "") problem |