# HG changeset patch
# User blanchet
# Date 1572013647 -7200
# Node ID ccc771091a78294003995f8659d057e5e2e0b72d
# Parent  718255bde391ffb493f72a008073d7b0ee085d0a
tuning

diff -r 718255bde391 -r ccc771091a78 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Fri Oct 25 16:26:56 2019 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Oct 25 16:27:27 2019 +0200
@@ -36,15 +36,15 @@
 val prefix = Library.prefix
 val fact_name_of = prefix fact_prefix o ascii_of
 
-fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
+fun atp_of_format (THF (Polymorphic, _)) = leo3N
   | atp_of_format (THF (Monomorphic, _)) = satallaxN
   | atp_of_format (DFG Polymorphic) = pirateN
   | atp_of_format (DFG Monomorphic) = spassN
   | atp_of_format (TFF Polymorphic) = alt_ergoN
   | atp_of_format (TFF Monomorphic) = vampireN
-  | atp_of_format FOF = eN
+  | atp_of_format FOF = eN (* FIXME? *)
   | atp_of_format CNF_UEQ = waldmeisterN
-  | atp_of_format CNF = eN
+  | atp_of_format CNF = eN (* FIXME? *)
 
 fun run_atp ctxt format problem =
   let
@@ -220,8 +220,7 @@
     val _ = app (File.append path) ss
   in () end
 
-fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc
-                                           file_name =
+fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc file_name =
   let
     val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc
     val ss = lines_of_problem ctxt format problem