# HG changeset patch
# User blanchet
# Date 1306854344 -7200
# Node ID 99bf2b38d3efda2eaa05b19f3f09636816033daf
# Parent  8c9046951dcb6bef34fceeeac9c9ac92f209f439
compile

diff -r 8c9046951dcb -r 99bf2b38d3ef src/HOL/ex/TPTP_Export.thy
--- 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};
diff -r 8c9046951dcb -r 99bf2b38d3ef src/HOL/ex/tptp_export.ML
--- 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),