src/HOL/TPTP/TPTP_Test.thy
changeset 47687 bfbd2d0bb348
parent 47558 55b42f9af99d
child 55595 2e2e9bc7c4c6
     1.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Mon Apr 23 12:23:23 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Mon Apr 23 12:23:23 2012 +0100
     1.3 @@ -35,15 +35,7 @@
     1.4      |> Path.expand;
     1.5  
     1.6    (*list of files to under test*)
     1.7 -  val files = TPTP_Syntax.get_file_list tptp_probs_dir;
     1.8 -
     1.9 -(*  (*test problem-name parsing and mangling*)
    1.10 -  val problem_names =
    1.11 -    map (Path.base #>
    1.12 -         Path.implode #>
    1.13 -         TPTP_Problem_Name.parse_problem_name #>
    1.14 -         TPTP_Problem_Name.mangle_problem_name)
    1.15 -        files*)
    1.16 +  fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir;
    1.17  *}
    1.18  
    1.19  
    1.20 @@ -82,7 +74,7 @@
    1.21      let
    1.22        fun f' x = (f x; ())
    1.23        val time =
    1.24 -        Timing.timing (List.app f') files
    1.25 +        Timing.timing (List.app f') (test_files ())
    1.26          |> fst
    1.27        val duration =
    1.28          #elapsed time
    1.29 @@ -90,7 +82,7 @@
    1.30          |> Real.fromLargeInt
    1.31        val average =
    1.32          (StringCvt.FIX (SOME 3),
    1.33 -         (duration / Real.fromInt (length files)))
    1.34 +         (duration / Real.fromInt (length (test_files ()))))
    1.35          |-> Real.fmt
    1.36      in
    1.37        report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^