1.1 --- a/src/HOL/ex/atp_export.ML	Mon Jun 27 14:56:26 2011 +0200
     1.2 +++ b/src/HOL/ex/atp_export.ML	Mon Jun 27 14:56:28 2011 +0200
     1.3 @@ -158,8 +158,8 @@
     1.4        facts0 |> map (fn ((_, loc), th) =>
     1.5                          ((Thm.get_name_hint th, loc), prop_of th))
     1.6      val (atp_problem, _, _, _, _, _, _) =
     1.7 -      prepare_atp_problem ctxt format Axiom Axiom type_sys true false true []
     1.8 -                          @{prop False} facts
     1.9 +      prepare_atp_problem ctxt format Axiom Axiom type_sys true true false true
    1.10 +                          [] @{prop False} facts
    1.11      val atp_problem =
    1.12        atp_problem
    1.13        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))