src/HOL/Tools/ATP/atp_util.ML

            | (0, _) => 0
            | (_, 0) => 0
            | (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 *)
         | Type ("Int.int", []) => 0 (* optimization *)
         | Type (s, _) =>