--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 22 13:17:59 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 22 14:28:22 2010 +0200
@@ -6,7 +6,6 @@
signature SLEDGEHAMMER_UTIL =
sig
- val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val replace_all : string -> string -> string -> string
@@ -24,8 +23,6 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
-fun pairf f g x = (f x, g x)
-
fun plural_s n = if n = 1 then "" else "s"
fun serial_commas _ [] = ["??"]