1.1 --- a/src/HOL/TPTP/atp_export.ML	Thu Jul 14 16:50:05 2011 +0200
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Thu Jul 14 16:50:05 2011 +0200
     1.3 @@ -159,8 +159,8 @@
     1.4      val (atp_problem, _, _, _, _, _, _) =
     1.5        facts
     1.6        |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
     1.7 -      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false
     1.8 -                             true [] @{prop False}
     1.9 +      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
    1.10 +                             combinatorsN false true [] @{prop False}
    1.11      val atp_problem =
    1.12        atp_problem
    1.13        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))