1.1 --- a/src/HOL/TPTP/atp_export.ML	Sun Jul 17 14:11:35 2011 +0200
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Sun Jul 17 14:12:45 2011 +0200
     1.3 @@ -160,8 +160,8 @@
     1.4        facts
     1.5        |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
     1.6        |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
     1.7 -                             (map (introduce_combinators ctxt o snd)) false true
     1.8 -                             [] @{prop False}
     1.9 +                             (rpair [] o map (introduce_combinators ctxt))
    1.10 +                             false true [] @{prop False}
    1.11      val atp_problem =
    1.12        atp_problem
    1.13        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))