diff -r 32f35b3d9e42 -r 55b42f9af99d src/HOL/TPTP/TPTP_Parser_Test.thy
--- 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");