118 val num_theorems = length name_thms_pairs |
118 val num_theorems = length name_thms_pairs |
119 val _ = priority ("Testing " ^ string_of_int num_theorems ^ |
119 val _ = priority ("Testing " ^ string_of_int num_theorems ^ |
120 " theorem" ^ plural_s num_theorems ^ "...") |
120 " theorem" ^ plural_s num_theorems ^ "...") |
121 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
121 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
122 val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
122 val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs |
123 val {context = ctxt, facts, goal} = Proof.goal state |
123 val {context = ctxt, facts, goal} = Proof.raw_goal state |
124 val problem = |
124 val problem = |
125 {subgoal = subgoal, goal = (ctxt, (facts, goal)), |
125 {subgoal = subgoal, goal = (ctxt, (facts, goal)), |
126 relevance_override = {add = [], del = [], only = false}, |
126 relevance_override = {add = [], del = [], only = false}, |
127 axiom_clauses = SOME axclauses, filtered_clauses = filtered} |
127 axiom_clauses = SOME axclauses, filtered_clauses = filtered} |
128 val (result, proof) = produce_answer (prover params timeout problem) |
128 val (result, proof) = produce_answer (prover params timeout problem) |