--- a/src/HOL/TPTP/atp_theory_export.ML Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jan 30 17:15:59 2012 +0100
@@ -180,8 +180,8 @@
|> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc),
th |> prop_of |> mono ? monomorphize_term ctxt))
- |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN
- false true [] @{prop False}
+ |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
+ true [] @{prop False}
|> #1
val atp_problem =
atp_problem