--- 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
()
*}