src/HOL/TPTP/ATP_Theory_Export.thy

--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Feb 05 17:43:15 2012 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Mon Feb 06 23:01:01 2012 +0100
@@ -22,9 +22,9 @@
 
 ML {*
 if do_it then
-  "/tmp/axs_mono_simple.dfg"
+  "/tmp/axs_mono_native.dfg"
   |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
-         "mono_simple"
+         "mono_native"
 else
   ()
 *}