--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 22:16:05 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 22:39:35 2012 +0200
@@ -2,8 +2,7 @@
Author: Nik Sultana, Cambridge University Computer Laboratory
Some tests for the TPTP interface. Some of the tests rely on the Isabelle
-environment variable TPTP_PROBLEMS_PATH, which should point to the
-TPTP-vX.Y.Z/Problems directory.
+environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
*)
theory TPTP_Interpret_Test
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 22:16:05 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 22:39:35 2012 +0200
@@ -832,10 +832,9 @@
Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
(Parse.path >> (fn path =>
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)))
+ (*NOTE: assumes include files are located at $TPTP/Axioms
+ (which is how TPTP is organised)*)
+ import_file true (Path.explode "$TPTP") path [] [] thy)))
(*Used for debugging. Returns all files contained within a directory or its
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 22:16:05 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 22:39:35 2012 +0200
@@ -9,7 +9,7 @@
uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
begin
-import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p"
+import_tptp "$TPTP/Problems/ALG/ALG001^5.p"
ML {*
val an_fmlas =
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy Wed Apr 18 22:16:05 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Wed Apr 18 22:39:35 2012 +0200
@@ -2,8 +2,7 @@
Author: Nik Sultana, Cambridge University Computer Laboratory
Some tests for the TPTP interface. Some of the tests rely on the Isabelle
-environment variable TPTP_PROBLEMS_PATH, which should point to the
-TPTP-vX.Y.Z/Problems directory.
+environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
*)
theory TPTP_Parser_Test
@@ -98,10 +97,10 @@
text "Parse a specific problem."
ML {*
map TPTP_Parser.parse_file
- ["$TPTP_PROBLEMS_PATH/FLD/FLD051-1.p",
- "$TPTP_PROBLEMS_PATH/FLD/FLD005-3.p",
- "$TPTP_PROBLEMS_PATH/SWV/SWV567-1.015.p",
- "$TPTP_PROBLEMS_PATH/SWV/SWV546-1.010.p"]
+ ["$TPTP/Problems/FLD/FLD051-1.p",
+ "$TPTP/Problems/FLD/FLD005-3.p",
+ "$TPTP/Problems/SWV/SWV567-1.015.p",
+ "$TPTP/Problems/SWV/SWV546-1.010.p"]
*}
ML {*
parser_test @{context} (situate "DAT/DAT001=1.p");
--- a/src/HOL/TPTP/TPTP_Test.thy Wed Apr 18 22:16:05 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Test.thy Wed Apr 18 22:39:35 2012 +0200
@@ -1,9 +1,8 @@
(* Title: HOL/TPTP/TPTP_Test.thy
Author: Nik Sultana, Cambridge University Computer Laboratory
-Some test support for the TPTP interface. Some of the tests rely on
-the Isabelle environment variable TPTP_PROBLEMS_PATH, which should
-point to the TPTP-vX.Y.Z/Problems directory.
+Some test support for the TPTP interface. Some of the tests rely on the Isabelle
+environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
*)
theory TPTP_Test
@@ -32,7 +31,7 @@
ML {*
(*problem source*)
val tptp_probs_dir =
- Path.explode "$TPTP_PROBLEMS_PATH"
+ Path.explode "$TPTP/Problems"
|> Path.expand;
(*list of files to under test*)