src/HOL/Tools/Metis/metis_translate.ML
changeset 45510 96696c360b3e
parent 45508 b216dc1b3630
child 45511 9b0f8ca4388e
equal deleted 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