--- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:03 2012 +0200
@@ -50,7 +50,11 @@
let
val thy = Proof_Context.theory_of ctxt
val prob_file = File.tmp_path (Path.explode "prob")
- val atp = case format of DFG _ => spassN | _ => eN
+ val atp =
+ case format of
+ DFG Polymorphic => spass_polyN
+ | DFG Monomorphic => spassN
+ | _ => eN
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy atp ()
val ord = effective_term_order ctxt atp