--- a/src/HOL/ex/TPTP_Export.thy Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/ex/TPTP_Export.thy Tue May 31 17:05:44 2011 +0200
@@ -3,8 +3,6 @@
uses "tptp_export.ML"
begin
-declare [[sledgehammer_atp_readable_names = false]]
-
ML {*
val do_it = false; (* switch to true to generate files *)
val thy = @{theory Complex_Main};
--- a/src/HOL/ex/tptp_export.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Tue May 31 17:05:44 2011 +0200
@@ -106,8 +106,8 @@
val explicit_apply = NONE
val (atp_problem, _, _, _, _, _, _) =
ATP_Translate.prepare_atp_problem ctxt format
- ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply []
- @{prop False} facts
+ ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
+ [] @{prop False} facts
val infers =
facts0 |> map (fn (_, (_, th)) =>
(fact_name_of (Thm.get_name_hint th),