src/HOL/Spec_Check/property.ML

--- a/src/HOL/Spec_Check/property.ML	Thu May 30 20:27:33 2013 +0200
+++ b/src/HOL/Spec_Check/property.ML	Thu May 30 20:38:50 2013 +0200
@@ -56,9 +56,13 @@
 
 fun classify' f =
   wrap (fn (x, result, {tags, count}) =>
-    { tags = if is_some result then
-        case f x of NONE => tags | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags
-      else tags, count = count })
+    { tags =
+        if is_some result then
+          (case f x of
+            NONE => tags
+          | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
+        else tags,
+     count = count })
 
 fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)