--- 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)))