# HG changeset patch
# User sultana
# Date 1335180203 -3600
# Node ID ba064cc165df9608914b4809ff20b9655e9793e8
# Parent  8b31786fe603b15a527902d0a041ae6c13cef008
removed redundant function;

diff -r 8b31786fe603 -r ba064cc165df src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Sun Apr 22 23:08:53 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 23 12:23:23 2012 +0100
@@ -110,11 +110,6 @@
   (*Imported TPTP files are stored as "manifests" in the theory.*)
   type manifest = TPTP_Problem_Name.problem_name * tptp_general_meaning
   val get_manifests : theory -> manifest list
-
-  (*Returns the list of all files included in a directory and its
-  subdirectories. This is only used for testing the parser/interpreter against
-  all TPTP problems.*)
-  val get_file_list : Path.T -> Path.T list
 end
 
 structure TPTP_Interpret : TPTP_INTERPRET =
@@ -867,29 +862,4 @@
          (which is how TPTP is organised)*)
        import_file true (Path.explode "$TPTP") path [] [] thy)))
 
-
-(*Used for debugging. Returns all files contained within a directory or its
-subdirectories. Follows symbolic links, filters away directories.*)
-fun get_file_list path =
-  let
-    fun check_file_entry f rest =
-      let
-        (*NOTE needed since don't have File.is_link and File.read_link*)
-        val f_str = Path.implode f
-      in
-        if File.is_dir f then
-          rest (*filter out directories*)
-        else if OS.FileSys.isLink f_str then
-          (*follow links -- NOTE this breaks if links are relative paths*)
-          check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest
-        else f :: rest
-      end
-  in
-    File.read_dir path
-    |> map
-        (Path.explode
-        #> Path.append path)
-    |> (fn l => fold check_file_entry l [])
-  end
-
 end