src/HOL/TPTP/TPTP_Parser_Test.thy

--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Mon Apr 23 12:23:23 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Mon Apr 23 12:23:23 2012 +0100
@@ -44,6 +44,14 @@
   val _ = map (fn (str, res) =>
     @{assert}(TPTP_Problem_Name.parse_problem_name str = res)) name_tests
 end
+
+(*test against all TPTP problems*)
+fun problem_names () =
+    map (Path.base #>
+         Path.implode #>
+         TPTP_Problem_Name.parse_problem_name #>
+         TPTP_Problem_Name.mangle_problem_name)
+        (test_files ())
 *}