src/HOL/ex/atp_export.ML

--- a/src/HOL/ex/atp_export.ML	Thu Jun 30 11:15:36 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Thu Jun 30 13:21:41 2011 +0200
@@ -112,7 +112,7 @@
 fun run_some_atp ctxt problem =
   let
     val thy = Proof_Context.theory_of ctxt
-    val prob_file = Path.explode "/tmp/prob.tptp"
+    val prob_file = Path.explode "/tmp/prob.tptp"  (* FIXME File.tmp_path (?) *)
     val {exec, arguments, proof_delims, known_failures, ...} =
       get_atp thy spassN
     val _ = problem |> tptp_lines_for_atp_problem FOF