--- a/src/HOL/TPTP/atp_export.ML Tue Aug 09 09:05:21 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Tue Aug 09 09:05:22 2011 +0200
@@ -160,8 +160,7 @@
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
- (rpair [] o map (introduce_combinators ctxt))
- false true [] @{prop False}
+ combinatorsN false true [] @{prop False}
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))