made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;

--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -154,7 +154,7 @@
 ML {*
   if test_all @{context} then
     (report @{context} "Interpreting all problems";
-     S timed_test (interpretation_test (get_timeout @{context})) @{context})
+     S timed_test (interpretation_test (get_timeout @{context})) @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
   else ()
 *}
 

--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -51,7 +51,7 @@
          Path.implode #>
          TPTP_Problem_Name.parse_problem_name #>
          TPTP_Problem_Name.mangle_problem_name)
-        (test_files ())
+     (TPTP_Syntax.get_file_list tptp_probs_dir)
 *}
 
 
@@ -121,7 +121,7 @@
 ML {*
   if test_all @{context} then
     (report @{context} "Testing parser";
-     S timed_test parser_test @{context})
+     S timed_test parser_test @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
   else ()
 *}
 

--- a/src/HOL/TPTP/TPTP_Test.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Test.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -33,9 +33,6 @@
   val tptp_probs_dir =
     Path.explode "$TPTP/Problems"
     |> Path.expand;
-
-  (*list of files to under test*)
-  fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir;
 *}
 
 
@@ -70,11 +67,11 @@
           default_val)
     end
 
-  fun timed_test ctxt f =
+  fun timed_test ctxt f test_files =
     let
       fun f' x = (f x; ())
       val time =
-        Timing.timing (List.app f') (test_files ())
+        Timing.timing (List.app f') test_files
         |> fst
       val duration =
         #elapsed time
@@ -82,7 +79,7 @@
         |> Real.fromLargeInt
       val average =
         (StringCvt.FIX (SOME 3),
-         (duration / Real.fromInt (length (test_files ()))))
+         (duration / Real.fromInt (length test_files)))
         |-> Real.fmt
     in
       report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^