equal
deleted
inserted
replaced
58 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
58 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
59 val axioms = maps (fn (n, ths) => map (pair n) ths) axioms |
59 val axioms = maps (fn (n, ths) => map (pair n) ths) axioms |
60 val {context = ctxt, goal, ...} = Proof.goal state |
60 val {context = ctxt, goal, ...} = Proof.goal state |
61 val problem = |
61 val problem = |
62 {ctxt = ctxt, goal = goal, subgoal = subgoal, |
62 {ctxt = ctxt, goal = goal, subgoal = subgoal, |
63 axiom_ts = map (prop_of o snd) axioms, |
63 axioms = map (prepare_axiom ctxt) axioms} |
64 prepared_axioms = map (prepare_axiom ctxt) axioms} |
|
65 val result as {outcome, used_thm_names, ...} = prover params (K "") problem |
64 val result as {outcome, used_thm_names, ...} = prover params (K "") problem |
66 in |
65 in |
67 priority (case outcome of |
66 priority (case outcome of |
68 NONE => |
67 NONE => |
69 if length used_thm_names = length axioms then |
68 if length used_thm_names = length axioms then |