src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 37414 d0cea0796295
parent 37321 9d7cfae95b30
child 37498 b426cbdb5a23
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jun 14 16:17:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jun 14 16:43:44 2010 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature SLEDGEHAMMER_UTIL =
     1.6  sig
     1.7 -  val is_new_spass_version : bool
     1.8    val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
     1.9    val plural_s : int -> string
    1.10    val serial_commas : string -> string list -> string list
    1.11 @@ -25,18 +24,6 @@
    1.12  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    1.13  struct
    1.14  
    1.15 -val is_new_spass_version =
    1.16 -  case getenv "SPASS_VERSION" of
    1.17 -    "" => (case getenv "SPASS_HOME" of
    1.18 -             "" => false
    1.19 -           | s =>
    1.20 -             (* Hack: Preliminary versions of the SPASS 3.7 package don't set
    1.21 -                "SPASS_VERSION". *)
    1.22 -             String.isSubstring "/spass-3.7/" s)
    1.23 -  | s => (case s |> space_explode "." |> map Int.fromString of
    1.24 -            SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
    1.25 -          | _ => false)
    1.26 -
    1.27  fun pairf f g x = (f x, g x)
    1.28  
    1.29  fun plural_s n = if n = 1 then "" else "s"