--- a/src/HOL/TPTP/atp_problem_import.ML Mon Jun 16 19:42:44 2014 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Mon Jun 16 19:44:02 2014 +0200
@@ -319,8 +319,8 @@
val presimp = true
val facts = map (apfst (rpair (Global, Non_Rec_Def))) defs @
map (apfst (rpair (Global, General))) nondefs
- val (atp_problem, _, _, _, _) =
- prepare_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
+ val (atp_problem, _, _, _) =
+ generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
lam_trans uncurried_aliases readable_names presimp [] conj facts
val ord = effective_term_order ctxt spassN
--- a/src/HOL/TPTP/atp_theory_export.ML Mon Jun 16 19:42:44 2014 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jun 16 19:44:02 2014 +0200
@@ -169,10 +169,9 @@
val problem =
facts
|> map (fn ((_, loc), th) =>
- ((Thm.get_name_hint th, loc),
- th |> prop_of |> mono ? monomorphize_term ctxt))
- |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
- false true [] @{prop False}
+ ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt))
+ |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
+ @{prop False}
|> #1 |> sort_wrt (heading_sort_key o fst)
val prelude = fst (split_last problem)
val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts