gracefully compute cardinality of sets (to avoid type protectors)

--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -192,6 +192,7 @@
            | (k1, k2) =>
              if k1 >= max orelse k2 >= max then max
              else Int.min (max, Integer.pow k2 k1))
+        | Type (@{type_name set}, [T']) => aux slack avoid (T' --> @{typ bool})
         | @{typ prop} => 2
         | @{typ bool} => 2 (* optimization *)
         | @{typ nat} => 0 (* optimization *)