# HG changeset patch
# User blanchet
# Date 1365513554 -7200
# Node ID 86e8c87e1f1b963814d69c13e3f7d828b87cee57
# Parent  8c38147d404e903f47c51840b76767be4fcb2620
tuning

diff -r 8c38147d404e -r 86e8c87e1f1b src/HOL/TPTP/ATP_Theory_Export.thy
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Apr 09 15:07:35 2013 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Apr 09 15:19:14 2013 +0200
@@ -33,8 +33,7 @@
 ML {*
 if do_it then
   "/tmp/infs_poly_guards_query_query.tptp"
-  |> generate_atp_inference_file_for_theory ctxt thy FOF
-         "poly_guards_query_query"
+  |> generate_atp_inference_file_for_theory ctxt thy FOF "poly_guards??"
 else
   ()
 *}
@@ -42,8 +41,7 @@
 ML {*
 if do_it then
   "/tmp/infs_poly_tags_query_query.tptp"
-  |> generate_atp_inference_file_for_theory ctxt thy FOF
-         "poly_tags_query_query"
+  |> generate_atp_inference_file_for_theory ctxt thy FOF "poly_tags??"
 else
   ()
 *}