--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 04 20:40:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 04 21:57:39 2012 +0100
@@ -896,7 +896,11 @@
val _ =
Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
(Parse.path >> (fn path =>
- Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
+ Toplevel.theory (fn thy =>
+ (*NOTE: assumes Axioms directory is on same level as the Problems one
+ (which is how TPTP is currently organised)*)
+ import_file true (Path.appends [Path.dir path, Path.parent, Path.parent])
+ path [] [] thy)))
(*Used for debugging. Returns all files contained within a directory or its