src/HOL/Tools/Metis/metis_translate.ML
changeset 43180 283114859d6c
parent 43175 4ca344fe0aca
child 43189 0ab7265f659f
equal deleted inserted replaced
43179:db5fb1d4df42 43180:283114859d6c
   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. *)