358 else |
358 else |
359 map (pair 0) |
359 map (pair 0) |
360 #> rpair ctxt |
360 #> rpair ctxt |
361 #-> Monomorph.monomorph Monomorph.all_schematic_consts_of |
361 #-> Monomorph.monomorph Monomorph.all_schematic_consts_of |
362 #> fst #> maps (map (zero_var_indexes o snd))) |
362 #> fst #> maps (map (zero_var_indexes o snd))) |
|
363 val (old_skolems, props) = |
|
364 fold_rev (fn clause => fn (old_skolems, props) => |
|
365 conceal_old_skolem_terms (length clauses) old_skolems |
|
366 (prop_of clause) |
|
367 ||> (fn prop => prop :: props)) |
|
368 clauses ([], []) |
363 val (atp_problem, _, _, _, _, _, sym_tab) = |
369 val (atp_problem, _, _, _, _, _, sym_tab) = |
364 prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply |
370 prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply |
365 false false (map prop_of clauses) @{prop False} [] |
371 false false props @{prop False} [] |
366 val axioms = |
372 val axioms = |
367 atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) |
373 atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) |
368 in |
374 in |
369 (MX, sym_tab, |
375 (MX, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems}) |
370 {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) |
|
371 end |
376 end |
372 | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = |
377 | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = |
373 let |
378 let |
374 val thy = Proof_Context.theory_of ctxt |
379 val thy = Proof_Context.theory_of ctxt |
375 (* The modes FO and FT are sticky. HO can be downgraded to FO. *) |
380 (* The modes FO and FT are sticky. HO can be downgraded to FO. *) |