--- a/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jun 26 11:14:40 2012 +0200
@@ -23,7 +23,7 @@
ML {*
if do_it then
"/tmp/axs_tc_native.dfg"
- |> generate_tptp_inference_file_for_theory ctxt thy (DFG With_Type_Classes)
+ |> generate_tptp_inference_file_for_theory ctxt thy (DFG Polymorphic)
"tc_native"
else
()
@@ -39,16 +39,9 @@
ML {*
if do_it then
- "/tmp/infs_poly_tags.tptp"
- |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags"
-else
- ()
-*}
-
-ML {*
-if do_it then
- "/tmp/infs_poly_tags_uniform.tptp"
- |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform"
+ "/tmp/infs_poly_tags_query_query.tptp"
+ |> generate_tptp_inference_file_for_theory ctxt thy FOF
+ "poly_tags_query_query"
else
()
*}