# HG changeset patch
# User blanchet
# Date 1402940642 -7200
# Node ID 027feff882c4bc7caa19bdcc9690f2172601382d
# Parent  8b87114357bdf0f2ee292913a7bfa4333713389c
compile

diff -r 8b87114357bd -r 027feff882c4 src/HOL/TPTP/atp_problem_import.ML
--- 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
diff -r 8b87114357bd -r 027feff882c4 src/HOL/TPTP/atp_theory_export.ML
--- 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