changeset 48141 | 1b864c4a3306 |
parent 48129 | 933d43c31689 |
child 48145 | f7b31782e632 |
--- 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 () *}