1.1 --- a/src/HOL/ex/atp_export.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/ex/atp_export.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -102,11 +102,10 @@
     1.4      val facts =
     1.5        facts0 |> map (fn ((_, loc), th) =>
     1.6                          ((Thm.get_name_hint th, loc), prop_of th))
     1.7 -    val explicit_apply = NONE
     1.8      val (atp_problem, _, _, _, _, _, _) =
     1.9        ATP_Translate.prepare_atp_problem ctxt format
    1.10 -          ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
    1.11 -          [] @{prop False} facts
    1.12 +          ATP_Problem.Axiom ATP_Problem.Axiom type_sys false true []
    1.13 +          @{prop False} facts
    1.14      val infers =
    1.15        facts0 |> map (fn (_, th) =>
    1.16                          (fact_name_of (Thm.get_name_hint th),