tuned;

--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Apr 04 21:57:39 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu Apr 05 00:37:22 2012 +0100
@@ -69,12 +69,12 @@
 section "Source problems"
 ML {*
   (*problem source*)
-  val thf_probs_dir =
+  val tptp_probs_dir =
     Path.explode "$TPTP_PROBLEMS_PATH"
     |> Path.expand;
 
   (*list of files to under test*)
-  val files = TPTP_Syntax.get_file_list thf_probs_dir;
+  val files = TPTP_Syntax.get_file_list tptp_probs_dir;
 
 (*  (*test problem-name parsing and mangling*)
   val problem_names =
@@ -140,7 +140,7 @@
 
 subsection "More parser tests"
 ML {*
-  fun situate file_name = Path.append thf_probs_dir (Path.explode file_name);
+  fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
   fun parser_test ctxt = (*FIXME argument order*)
     test_fn ctxt
      (fn file_name =>
@@ -184,8 +184,8 @@
     Timing.timing
     (TPTP_Interpret.interpret_file
      false
-     (Path.dir thf_probs_dir)
-    (Path.append thf_probs_dir (Path.explode "LCL/LCL825-1.p"))
+     (Path.dir tptp_probs_dir)
+    (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
      []
      [])
     @{theory}
@@ -228,7 +228,7 @@
        TimeLimit.timeLimit (Time.fromSeconds timeout)
        (TPTP_Interpret.interpret_file
          false
-         (Path.dir thf_probs_dir)
+         (Path.dir tptp_probs_dir)
          file
          []
          [])