--- a/src/HOL/TPTP/atp_theory_export.ML Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Mon May 21 10:39:32 2012 +0200
@@ -183,8 +183,8 @@
|> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc),
th |> prop_of |> mono ? monomorphize_term ctxt))
- |> prepare_atp_problem ctxt format Axiom type_enc true combsN false false
- true [] @{prop False}
+ |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
+ false true [] @{prop False}
|> #1
val atp_problem =
atp_problem