author | paulson |
Thu, 12 Oct 2006 15:48:13 +0200 | |
changeset 20995 | 51c41f167adc |
parent 20994 | 6f2995b4c867 |
child 20996 | 197e6875d637 |
--- 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*)