src/HOL/TPTP/TPTP_Parser_Test.thy
changeset 55595 2e2e9bc7c4c6
parent 47687 bfbd2d0bb348
child 62390 842917225d56
--- 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 ()
 *}