src/HOL/TPTP/ATP_Export.thy

--- a/src/HOL/TPTP/ATP_Export.thy	Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/TPTP/ATP_Export.thy	Sat Oct 29 13:51:35 2011 +0200
@@ -4,6 +4,11 @@
 begin
 
 ML {*
+open ATP_Problem;
+open ATP_Export;
+*}
+
+ML {*
 val do_it = false; (* switch to "true" to generate the files *)
 val thy = @{theory Complex_Main};
 val ctxt = @{context}
@@ -11,32 +16,40 @@
 
 ML {*
 if do_it then
-  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds"
-      "/tmp/infs_poly_preds.tptp"
+  "/tmp/axs_mono_simple.dfg"
+  |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
+         "mono_simple"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags"
-      "/tmp/infs_poly_tags.tptp"
+  "/tmp/infs_poly_guards.tptp"
+  |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_uniform"
-      "/tmp/infs_poly_tags_uniform.tptp"
+  "/tmp/infs_poly_tags.tptp"
+  |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  ATP_Export.generate_tptp_graph_file_for_theory ctxt thy
-      "/tmp/graph.out"
+  "/tmp/infs_poly_tags_uniform.tptp"
+  |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform"
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  "/tmp/graph.out" |> generate_tptp_graph_file_for_theory ctxt thy
 else
   ()
 *}