src/HOL/TPTP/ATP_Theory_Export.thy
changeset 47263 e9c90516bc0d
parent 47149 484dc68c8c89
child 49144 933d43c31689
     1.1 --- a/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Feb 05 17:43:15 2012 +0100
     1.2 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Mon Feb 06 23:01:01 2012 +0100
     1.3 @@ -22,9 +22,9 @@
     1.4  
     1.5  ML {*
     1.6  if do_it then
     1.7 -  "/tmp/axs_mono_simple.dfg"
     1.8 +  "/tmp/axs_mono_native.dfg"
     1.9    |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted)
    1.10 -         "mono_simple"
    1.11 +         "mono_native"
    1.12  else
    1.13    ()
    1.14  *}