src/HOL/Tools/Metis/metis_translate.ML
 changeset 45510 96696c360b3e parent 45508 b216dc1b3630 child 45511 9b0f8ca4388e
equal inserted replaced
45509:624872fc47bf 45510:96696c360b3e
`   225       if lambda_trans = combinatorsN then (no_lambdasN, false)`
`   225       if lambda_trans = combinatorsN then (no_lambdasN, false)`
`   226       else (lambda_trans, true)`
`   226       else (lambda_trans, true)`
`   227     val (atp_problem, _, _, _, _, _, lifted, sym_tab) =`
`   227     val (atp_problem, _, _, _, _, _, lifted, sym_tab) =`
`   228       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans`
`   228       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans`
`   229                           false preproc [] @{prop False} props`
`   229                           false preproc [] @{prop False} props`
`       `
`   230     (*`
`   230     val _ = tracing ("ATP PROBLEM: " ^`
`   231     val _ = tracing ("ATP PROBLEM: " ^`
`   231                      cat_lines (lines_for_atp_problem CNF atp_problem))`
`   232                      cat_lines (lines_for_atp_problem CNF atp_problem))`
`       `
`   233     *)`
`   232     (* "rev" is for compatibility with existing proof scripts. *)`
`   234     (* "rev" is for compatibility with existing proof scripts. *)`
`   233     val axioms =`
`   235     val axioms =`
`   234       atp_problem`
`   236       atp_problem`
`   235       |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev`
`   237       |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev`
`   236   in (sym_tab, axioms, (lifted, old_skolems)) end`
`   238   in (sym_tab, axioms, (lifted, old_skolems)) end`