src/HOL/Tools/Metis/metis_translate.ML
changeset 43190 494fde207706
parent 43189 0ab7265f659f
child 43193 e11bd628f1a5
equal deleted inserted replaced
43189:0ab7265f659f 43190:494fde207706
   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) =
   363       val (old_skolems, props) =
   364         fold_rev (fn clause => fn (old_skolems, props) =>
   364         fold_rev (fn clause => fn (old_skolems, props) =>
   365                      conceal_old_skolem_terms (length clauses) old_skolems
   365                      clause |> prop_of |> Logic.strip_imp_concl
   366                                               (prop_of clause)
   366                             |> conceal_old_skolem_terms (length clauses)
   367                      ||> (fn prop => prop :: props))
   367                                                         old_skolems
       
   368                             ||> (fn prop => prop :: props))
   368              clauses ([], [])
   369              clauses ([], [])
   369       val (atp_problem, _, _, _, _, _, sym_tab) =
   370       val (atp_problem, _, _, _, _, _, sym_tab) =
   370         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
   371         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
   371                             false false props @{prop False} []
   372                             false false props @{prop False} []
   372       val axioms =
   373       val axioms =