src/HOL/Tools/res_lib.ML
changeset 17764 fde495b9e24b
parent 17525 ae5bb6001afb
child 17775 2679ba74411f
     1.1 --- a/src/HOL/Tools/res_lib.ML	Wed Oct 05 10:56:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_lib.ML	Wed Oct 05 11:18:06 2005 +0200
     1.3 @@ -10,12 +10,8 @@
     1.4  sig
     1.5  val flat_noDup : ''a list list -> ''a list
     1.6  val helper_path : string -> string -> string
     1.7 -val list2str_sep : string -> string list -> string
     1.8  val no_rep_add : ''a -> ''a list -> ''a list
     1.9  val no_rep_app : ''a list -> ''a list -> ''a list
    1.10 -val pair_ins : 'a -> 'b list -> ('a * 'b) list
    1.11 -val write_strs : TextIO.outstream -> TextIO.vector list -> unit
    1.12 -val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
    1.13  val intOfPid : Posix.Process.pid -> Int.int
    1.14  val pidOfInt : Int.int -> Posix.Process.pid
    1.15  end;
    1.16 @@ -33,19 +29,7 @@
    1.17  fun flat_noDup []     = []
    1.18    | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
    1.19  
    1.20 -fun list2str_sep delim []      = delim
    1.21 -  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
    1.22 -
    1.23 -fun write_strs _   []      = ()
    1.24 -  | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
    1.25 -
    1.26 -fun writeln_strs _   []      = ()
    1.27 -  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
    1.28 -
    1.29 -(* pair the first argument with each element in the second input list *)
    1.30 -fun pair_ins x []      = []
    1.31 -  | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
    1.32 -  
    1.33 + 
    1.34  (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    1.35    it exists. --lcp *)  
    1.36  fun helper_path evar base =