# HG changeset patch
# User blanchet
# Date 1334999749 -7200
# Node ID 2d90e10f61f21a60dc851a699697476d14c1bf4e
# Parent  e33c2be488fe4d9c1e7024d2dd1f246e71a0e2b6
prepend PWD to relative paths

diff -r e33c2be488fe -r 2d90e10f61f2 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Sat Apr 21 11:15:49 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Sat Apr 21 11:15:49 2012 +0200
@@ -123,7 +123,13 @@
     |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not
 
 fun read_tptp_file thy file_name =
-  let val path = Path.explode file_name in
+  let
+    val path =
+      Path.explode file_name
+      |> (fn path =>
+             path |> not (Path.is_absolute path)
+                     ? Path.append (Path.explode "$PWD"))
+  in
     (case parse_tptp_problem (File.read path) of
        (_, s :: ss) =>
        raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))