equal
deleted
inserted
replaced
178 *) |
178 *) |
179 val (atp_problem, _, _, _, _, _, sym_tab) = |
179 val (atp_problem, _, _, _, _, _, sym_tab) = |
180 prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply |
180 prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply |
181 false false props @{prop False} [] |
181 false false props @{prop False} [] |
182 (* |
182 (* |
183 val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem)) |
183 val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) |
184 *) |
184 *) |
185 (* "rev" is for compatibility *) |
185 (* "rev" is for compatibility *) |
186 val axioms = |
186 val axioms = |
187 atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) |
187 atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) |
188 |> rev |
188 |> rev |