1.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Mon Jun 16 19:42:44 2014 +0200
     1.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Jun 16 19:44:02 2014 +0200
     1.3 @@ -319,8 +319,8 @@
     1.4      val presimp = true
     1.5      val facts = map (apfst (rpair (Global, Non_Rec_Def))) defs @
     1.6        map (apfst (rpair (Global, General))) nondefs
     1.7 -    val (atp_problem, _, _, _, _) =
     1.8 -      prepare_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
     1.9 +    val (atp_problem, _, _, _) =
    1.10 +      generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
    1.11          lam_trans uncurried_aliases readable_names presimp [] conj facts
    1.12  
    1.13      val ord = effective_term_order ctxt spassN

     2.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jun 16 19:42:44 2014 +0200
     2.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jun 16 19:44:02 2014 +0200
     2.3 @@ -169,10 +169,9 @@
     2.4      val problem =
     2.5        facts
     2.6        |> map (fn ((_, loc), th) =>
     2.7 -                 ((Thm.get_name_hint th, loc),
     2.8 -                   th |> prop_of |> mono ? monomorphize_term ctxt))
     2.9 -      |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
    2.10 -                             false true [] @{prop False}
    2.11 +        ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt))
    2.12 +      |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
    2.13 +        @{prop False}
    2.14        |> #1 |> sort_wrt (heading_sort_key o fst)
    2.15      val prelude = fst (split_last problem)
    2.16      val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts