# HG changeset patch
# User blanchet
# Date 1272464096 -7200
# Node ID 8b2dc9b4bf4cedc5249548e804382be288a324d3
# Parent  afb63db6249c72cba3124a79c8b1dbc3778562e3
parentheses around nested cases

diff -r afb63db6249c -r 8b2dc9b4bf4c src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 16:06:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Apr 28 16:14:56 2010 +0200
@@ -25,15 +25,15 @@
 
 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
+    "" => (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)