--- a/src/HOL/ex/tptp_export.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Mon May 30 17:00:38 2011 +0200
@@ -103,7 +103,7 @@
facts0 |> map_filter (try (fn ((_, loc), (_, th)) =>
Sledgehammer_ATP_Translate.translate_atp_fact ctxt format
type_sys true ((Thm.get_name_hint th, loc), th)))
- val explicit_apply = false
+ val explicit_apply = NONE
val (atp_problem, _, _, _, _, _, _) =
Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format
ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply []