src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

 General-purpose functions used by the Sledgehammer modules.
 *)
 
 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
   val replace_all : string -> string -> string -> string
   val remove_all : string -> string -> string

   val specialize_type : theory -> (string * typ) -> term -> term
 end;
  
 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"