diff -r 016ce79deb01 -r b381d428a725 src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Tue Apr 17 16:14:07 2012 +0100
@@ -7,21 +7,12 @@
 *)
 
 theory TPTP_Parser_Test
-imports TPTP_Parser TPTP_Parser_Example
+imports TPTP_Test (*TPTP_Parser_Example*)
 begin
 
-ML {*
-  val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "")
-  fun S x y z = x z (y z)
-*}
-
 section "Parser tests"
 
 ML {*
-  fun payload_of (TPTP_Syntax.Annotated_Formula (_, _, _, _, fmla, _)) = fmla
-  val payloads_of = map payload_of
-*}
-ML {*
   TPTP_Parser.parse_expression "" "fof(dt_k4_waybel34, axiom, ~ v3).";
   TPTP_Parser.parse_expression "" "thf(dt_k4_waybel34, axiom, ~ ($true | $false)).";
   TPTP_Parser.parse_expression ""
@@ -66,94 +57,6 @@
 *}
 
 
-section "Source problems"
-ML {*
-  (*problem source*)
-  val tptp_probs_dir =
-    Path.explode "$TPTP_PROBLEMS_PATH"
-    |> Path.expand;
-
-  (*list of files to under test*)
-  val files = TPTP_Syntax.get_file_list tptp_probs_dir;
-
-(*  (*test problem-name parsing and mangling*)
-  val problem_names =
-    map (Path.base #>
-         Path.implode #>
-         TPTP_Problem_Name.parse_problem_name #>
-         TPTP_Problem_Name.mangle_problem_name)
-        files*)
-*}
-
-
-section "Supporting test functions"
-ML {*
-  fun report ctxt str =
-    let
-      val warning_out = Config.get ctxt warning_out
-    in
-      if warning_out = "" then warning str
-      else
-        let
-          val out_stream = TextIO.openAppend warning_out
-        in (TextIO.output (out_stream, str ^ "\n");
-            TextIO.flushOut out_stream;
-            TextIO.closeOut out_stream)
-        end
-    end
-
-  fun test_fn ctxt f msg default_val file_name =
-    let
-      val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
-    in
-     (f file_name; ())
-     (*otherwise report exceptions as warnings*)
-     handle exn =>
-       if Exn.is_interrupt exn then
-         reraise exn
-       else
-         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
-          " raised exception: " ^ ML_Compiler.exn_message exn);
-          default_val)
-    end
-
-  fun timed_test ctxt f =
-    let
-      fun f' x = (f x; ())
-      val time =
-        Timing.timing (List.app f') files
-        |> fst
-      val duration =
-        #elapsed time
-        |> Time.toSeconds
-        |> Real.fromLargeInt
-      val average =
-        (StringCvt.FIX (SOME 3),
-         (duration / Real.fromInt (length files)))
-        |-> Real.fmt
-    in
-      report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^
-       "s per problem)")
-    end
-*}
-
-
-subsection "More parser tests"
-ML {*
-  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 =>
-        Path.implode file_name
-        |> (fn file =>
-             ((*report ctxt file; this is if you want the filename in the log*)
-              TPTP_Parser.parse_file file)))
-     "parser"
-     ()
-*}
-
-declare [[warning_out = ""]]
-
 text "Parse a specific problem."
 ML {*
   map TPTP_Parser.parse_file
@@ -176,66 +79,4 @@
 *}
 
 
-subsection "Interpretation"
-
-text "Interpret a problem."
-ML {*
-  val (time, ((type_map, const_map, fmlas), thy)) =
-    Timing.timing
-    (TPTP_Interpret.interpret_file
-     false
-     (Path.dir tptp_probs_dir)
-    (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
-     []
-     [])
-    @{theory}
-
-  (*also tried
-     "ALG/ALG001^5.p"
-     "COM/COM003+2.p"
-     "COM/COM003-1.p"
-     "COM/COM024^5.p"
-     "DAT/DAT017=1.p"
-     "NUM/NUM021^1.p"
-     "NUM/NUM858=1.p"
-     "SYN/SYN000^2.p"*)
-
- (*These take too long
-    "NLP/NLP562+1.p"
-    "SWV/SWV546-1.010.p"
-    "SWV/SWV567-1.015.p"
-    "LCL/LCL680+1.020.p"*)
-*}
-
-text "... and display nicely."
-ML {*
-  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
-*}
-ML {*
-  (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
-  List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
-*}
-
-
-text "Run interpretation over all problems. This works only for logics
- for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
-ML {*
-  report @{context} "Interpreting all problems.";
-  fun interpretation_test timeout ctxt =
-    test_fn ctxt
-     (fn file =>
-      (writeln (Path.implode file);
-       TimeLimit.timeLimit (Time.fromSeconds timeout)
-       (TPTP_Interpret.interpret_file
-         false
-         (Path.dir tptp_probs_dir)
-         file
-         []
-         [])
-         @{theory}))
-     "interpreter"
-     ()
-  val _ = S timed_test (interpretation_test 5) @{context}
-*}
-
 end
\ No newline at end of file