src/HOL/TPTP/atp_export.ML

--- a/src/HOL/TPTP/atp_export.ML	Sun Jul 17 08:45:06 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Sun Jul 17 14:11:34 2011 +0200
@@ -160,7 +160,8 @@
       facts
       |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
       |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
-                             combinatorsN false true [] @{prop False}
+                             (map (introduce_combinators ctxt)) false true []
+                             @{prop False}
     val atp_problem =
       atp_problem
       |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))