# HG changeset patch
# User paulson
# Date 1160660893 -7200
# Node ID 51c41f167adc890056b300c535d7d4e91594393c
# Parent  6f2995b4c867fc0ed54cdea07f4ec064c472e507
Logging of theorem names to the /tmp directory now works

diff -r 6f2995b4c867 -r 51c41f167adc src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Oct 12 15:00:07 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Oct 12 15:48:13 2006 +0200
@@ -756,7 +756,7 @@
   end
   
 fun trace_array fname =
-  let val path = File.tmp_path (Path.basic fname)
+  let val path = File.unpack_platform_path fname
   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
 
 (*Converting a subgoal into negated conjecture clauses*)