# HG changeset patch
# User blanchet
# Date 1340702080 -7200
# Node ID f7b31782e632553996a5353a998031f1a6477c32
# Parent  b3c5c5361e80cd54857c94903b65c4bb9e37b8a0
compile

diff -r b3c5c5361e80 -r f7b31782e632 src/HOL/TPTP/ATP_Theory_Export.thy
--- 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
   ()
 *}