--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 14 16:17:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jun 14 16:43:44 2010 +0200
@@ -6,7 +6,6 @@
signature SLEDGEHAMMER_UTIL =
sig
- val is_new_spass_version : bool
val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val plural_s : int -> string
val serial_commas : string -> string list -> string list
@@ -25,18 +24,6 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
-val is_new_spass_version =
- case getenv "SPASS_VERSION" of
- "" => (case getenv "SPASS_HOME" of
- "" => false
- | s =>
- (* Hack: Preliminary versions of the SPASS 3.7 package don't set
- "SPASS_VERSION". *)
- String.isSubstring "/spass-3.7/" s)
- | s => (case s |> space_explode "." |> map Int.fromString of
- SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
- | _ => false)
-
fun pairf f g x = (f x, g x)
fun plural_s n = if n = 1 then "" else "s"