src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 37498 b426cbdb5a23
parent 37414 d0cea0796295
child 37575 cfc5e281740f
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 22 13:17:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 22 14:28:22 2010 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature SLEDGEHAMMER_UTIL =
     1.6  sig
     1.7 -  val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
     1.8    val plural_s : int -> string
     1.9    val serial_commas : string -> string list -> string list
    1.10    val replace_all : string -> string -> string -> string
    1.11 @@ -24,8 +23,6 @@
    1.12  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    1.13  struct
    1.14  
    1.15 -fun pairf f g x = (f x, g x)
    1.16 -
    1.17  fun plural_s n = if n = 1 then "" else "s"
    1.18  
    1.19  fun serial_commas _ [] = ["??"]