src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36496 8b2dc9b4bf4c
parent 36491 6769f8eacaac
child 36555 8ff45c2076da
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 16:06:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 16:14:56 2010 +0200
     1.3 @@ -25,15 +25,15 @@
     1.4  
     1.5  val is_new_spass_version =
     1.6    case getenv "SPASS_VERSION" of
     1.7 -    "" => case getenv "SPASS_HOME" of
     1.8 -            "" => false
     1.9 -          | s =>
    1.10 -            (* Hack: Preliminary versions of the SPASS 3.7 package don't set
    1.11 -               "SPASS_VERSION". *)
    1.12 -            String.isSubstring "/spass-3.7/" s
    1.13 -  | s => case s |> space_explode "." |> map Int.fromString of
    1.14 -           SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
    1.15 -         | _ => false
    1.16 +    "" => (case getenv "SPASS_HOME" of
    1.17 +             "" => false
    1.18 +           | s =>
    1.19 +             (* Hack: Preliminary versions of the SPASS 3.7 package don't set
    1.20 +                "SPASS_VERSION". *)
    1.21 +             String.isSubstring "/spass-3.7/" s)
    1.22 +  | s => (case s |> space_explode "." |> map Int.fromString of
    1.23 +            SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
    1.24 +          | _ => false)
    1.25  
    1.26  fun pairf f g x = (f x, g x)
    1.27