src/HOL/TPTP/ATP_Theory_Export.thy

--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Tue Jun 26 11:14:40 2012 +0200
@@ -22,8 +22,9 @@
 
 ML {*
 if do_it then
-  "/tmp/axs_mono_native.dfg"
-  |> generate_tptp_inference_file_for_theory ctxt thy DFG "mono_native"
+  "/tmp/axs_tc_native.dfg"
+  |> generate_tptp_inference_file_for_theory ctxt thy (DFG With_Type_Classes)
+                                             "tc_native"
 else
   ()
 *}