1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 22:16:05 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Apr 18 22:39:35 2012 +0200
     1.3 @@ -2,8 +2,7 @@
     1.4      Author:     Nik Sultana, Cambridge University Computer Laboratory
     1.5  
     1.6  Some tests for the TPTP interface. Some of the tests rely on the Isabelle
     1.7 -environment variable TPTP_PROBLEMS_PATH, which should point to the
     1.8 -TPTP-vX.Y.Z/Problems directory.
     1.9 +environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
    1.10  *)
    1.11  
    1.12  theory TPTP_Interpret_Test

     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 18 22:16:05 2012 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 18 22:39:35 2012 +0200
     2.3 @@ -832,10 +832,9 @@
     2.4    Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
     2.5      (Parse.path >> (fn path =>
     2.6        Toplevel.theory (fn thy =>
     2.7 -       (*NOTE: assumes Axioms directory is on same level as the Problems one
     2.8 -         (which is how TPTP is currently organised)*)
     2.9 -       import_file true (Path.appends [Path.dir path, Path.parent, Path.parent])
    2.10 -        path [] [] thy)))
    2.11 +       (*NOTE: assumes include files are located at $TPTP/Axioms
    2.12 +         (which is how TPTP is organised)*)
    2.13 +       import_file true (Path.explode "$TPTP") path [] [] thy)))
    2.14  
    2.15  
    2.16  (*Used for debugging. Returns all files contained within a directory or its

     3.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Apr 18 22:16:05 2012 +0200
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Apr 18 22:39:35 2012 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
     3.5  begin
     3.6  
     3.7 -import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p"
     3.8 +import_tptp "$TPTP/Problems/ALG/ALG001^5.p"
     3.9  
    3.10  ML {*
    3.11  val an_fmlas =

     4.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Apr 18 22:16:05 2012 +0200
     4.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Apr 18 22:39:35 2012 +0200
     4.3 @@ -2,8 +2,7 @@
     4.4      Author:     Nik Sultana, Cambridge University Computer Laboratory
     4.5  
     4.6  Some tests for the TPTP interface. Some of the tests rely on the Isabelle
     4.7 -environment variable TPTP_PROBLEMS_PATH, which should point to the
     4.8 -TPTP-vX.Y.Z/Problems directory.
     4.9 +environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
    4.10  *)
    4.11  
    4.12  theory TPTP_Parser_Test
    4.13 @@ -98,10 +97,10 @@
    4.14  text "Parse a specific problem."
    4.15  ML {*
    4.16    map TPTP_Parser.parse_file
    4.17 -   ["$TPTP_PROBLEMS_PATH/FLD/FLD051-1.p",
    4.18 -    "$TPTP_PROBLEMS_PATH/FLD/FLD005-3.p",
    4.19 -    "$TPTP_PROBLEMS_PATH/SWV/SWV567-1.015.p",
    4.20 -    "$TPTP_PROBLEMS_PATH/SWV/SWV546-1.010.p"]
    4.21 +   ["$TPTP/Problems/FLD/FLD051-1.p",
    4.22 +    "$TPTP/Problems/FLD/FLD005-3.p",
    4.23 +    "$TPTP/Problems/SWV/SWV567-1.015.p",
    4.24 +    "$TPTP/Problems/SWV/SWV546-1.010.p"]
    4.25  *}
    4.26  ML {*
    4.27    parser_test @{context} (situate "DAT/DAT001=1.p");

     5.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Wed Apr 18 22:16:05 2012 +0200
     5.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Wed Apr 18 22:39:35 2012 +0200
     5.3 @@ -1,9 +1,8 @@
     5.4  (*  Title:      HOL/TPTP/TPTP_Test.thy
     5.5      Author:     Nik Sultana, Cambridge University Computer Laboratory
     5.6  
     5.7 -Some test support for the TPTP interface. Some of the tests rely on
     5.8 -the Isabelle environment variable TPTP_PROBLEMS_PATH, which should
     5.9 -point to the TPTP-vX.Y.Z/Problems directory.
    5.10 +Some test support for the TPTP interface. Some of the tests rely on the Isabelle
    5.11 +environment variable $TPTP, which should point to the TPTP-vX.Y.Z directory.
    5.12  *)
    5.13  
    5.14  theory TPTP_Test
    5.15 @@ -32,7 +31,7 @@
    5.16  ML {*
    5.17    (*problem source*)
    5.18    val tptp_probs_dir =
    5.19 -    Path.explode "$TPTP_PROBLEMS_PATH"
    5.20 +    Path.explode "$TPTP/Problems"
    5.21      |> Path.expand;
    5.22  
    5.23    (*list of files to under test*)