--- a/src/HOL/TPTP/atp_theory_export.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Mar 04 19:53:18 2015 +0100
@@ -170,7 +170,7 @@
val problem =
facts
|> map (fn ((_, loc), th) =>
- ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt))
+ ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
|> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
@{prop False}
|> #1 |> sort_wrt (heading_sort_key o fst)