src/HOL/TPTP/ATP_Theory_Export.thy

--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -5,7 +5,7 @@
 header {* ATP Theory Exporter *}
 
 theory ATP_Theory_Export
-imports Complex_Main
+imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
 uses "atp_theory_export.ML"
 begin
 
@@ -15,13 +15,22 @@
 *}
 
 ML {*
-val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory};
+val do_it = true; (* switch to "true" to generate the files *)
+val thy = @{theory List};
 val ctxt = @{context}
 *}
 
 ML {*
 if do_it then
+  "/tmp/axs_tc_native.dfg"
+  |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
+         "tc_native"
+else
+  ()
+*}
+
+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"
@@ -38,13 +47,4 @@
   ()
 *}
 
-ML {*
-if do_it then
-  "/tmp/axs_tc_native.dfg"
-  |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
-         "tc_native"
-else
-  ()
-*}
-
 end