# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID 0feb93dfb268230da5d6f5314d511cf18c37dd33
# Parent  141ab3c13ac84ed08623f4cbf5be1a953a09481a
gracefully compute cardinality of sets (to avoid type protectors)

diff -r 141ab3c13ac8 -r 0feb93dfb268 src/HOL/Tools/ATP/atp_util.ML
--- 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 *)