improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
authorblanchet
Mon Feb 28 17:53:10 2011 +0100 (2011-02-28)
changeset 4186049d0fc8c418c
parent 41859 c3a5912d0922
child 41861 77d87dc50e5a
improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 28 17:53:10 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 28 17:53:10 2011 +0100
     1.3 @@ -66,12 +66,6 @@
     1.4    val strip_first_name_sep : string -> string * string
     1.5    val original_name : string -> string
     1.6    val abs_var : indexname * typ -> term -> term
     1.7 -  val is_higher_order_type : typ -> bool
     1.8 -  val is_special_eligible_arg : bool -> typ list -> term -> bool
     1.9 -  val s_let :
    1.10 -    typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
    1.11 -  val s_betapply : typ list -> term * term -> term
    1.12 -  val s_betapplys : typ list -> term * term list -> term
    1.13    val s_conj : term * term -> term
    1.14    val s_disj : term * term -> term
    1.15    val strip_any_connective : term -> term list * term
    1.16 @@ -105,6 +99,7 @@
    1.17    val is_integer_like_type : typ -> bool
    1.18    val is_record_type : typ -> bool
    1.19    val is_number_type : Proof.context -> typ -> bool
    1.20 +  val is_higher_order_type : typ -> bool
    1.21    val const_for_iterator_type : typ -> styp
    1.22    val strip_n_binders : int -> typ -> typ list * typ
    1.23    val nth_range_type : int -> typ -> typ
    1.24 @@ -165,6 +160,18 @@
    1.25    val num_datatype_constrs : hol_context -> typ -> int
    1.26    val constr_name_for_sel_like : string -> string
    1.27    val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
    1.28 +  val card_of_type : (typ * int) list -> typ -> int
    1.29 +  val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
    1.30 +  val bounded_exact_card_of_type :
    1.31 +    hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
    1.32 +  val typical_card_of_type : typ -> int
    1.33 +  val is_finite_type : hol_context -> typ -> bool
    1.34 +  val is_small_finite_type : hol_context -> typ -> bool
    1.35 +  val is_special_eligible_arg : bool -> typ list -> term -> bool
    1.36 +  val s_let :
    1.37 +    typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
    1.38 +  val s_betapply : typ list -> term * term -> term
    1.39 +  val s_betapplys : typ list -> term * term list -> term
    1.40    val discriminate_value : hol_context -> styp -> term -> term
    1.41    val select_nth_constr_arg :
    1.42      Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
    1.43 @@ -172,12 +179,6 @@
    1.44    val construct_value :
    1.45      Proof.context -> (typ option * bool) list -> styp -> term list -> term
    1.46    val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
    1.47 -  val card_of_type : (typ * int) list -> typ -> int
    1.48 -  val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
    1.49 -  val bounded_exact_card_of_type :
    1.50 -    hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
    1.51 -  val is_finite_type : hol_context -> typ -> bool
    1.52 -  val is_small_finite_type : hol_context -> typ -> bool
    1.53    val special_bounds : term list -> (indexname * typ) list
    1.54    val is_funky_typedef : Proof.context -> typ -> bool
    1.55    val all_axioms_of :
    1.56 @@ -327,82 +328,6 @@
    1.57    else
    1.58      s
    1.59  
    1.60 -val evil_nix = 0
    1.61 -val evil_prod = 1
    1.62 -val evil_fun = 2
    1.63 -
    1.64 -(* Returns an approximation of how evil a type is (i.e., how much are we willing
    1.65 -   to try to specialize the argument even if it contains bound variables). *)
    1.66 -fun type_evil (Type (@{type_name fun}, _)) = evil_fun
    1.67 -  | type_evil (Type (s, Ts)) =
    1.68 -    (if s = @{type_name prod} then evil_prod else evil_nix)
    1.69 -    |> fold (Integer.max o type_evil) Ts
    1.70 -  | type_evil _ = evil_nix
    1.71 -
    1.72 -fun is_higher_order_type T = (type_evil T = evil_fun)
    1.73 -
    1.74 -fun is_special_eligible_arg strict Ts t =
    1.75 -  case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
    1.76 -    [] => true
    1.77 -  | bad_Ts =>
    1.78 -    case type_evil (fastype_of1 (Ts, t)) of
    1.79 -      0 => false
    1.80 -    | T_evil =>
    1.81 -      let val bad_Ts_evil = fold (Integer.max o type_evil) bad_Ts evil_nix in
    1.82 -        (bad_Ts_evil, T_evil) |> (if strict then op < else op <=)
    1.83 -      end
    1.84 -
    1.85 -fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    1.86 -
    1.87 -fun let_var s = (nitpick_prefix ^ s, 999)
    1.88 -val let_inline_threshold = 20
    1.89 -
    1.90 -fun s_let Ts s n abs_T body_T f t =
    1.91 -  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
    1.92 -     is_special_eligible_arg false Ts t then
    1.93 -    f t
    1.94 -  else
    1.95 -    let val z = (let_var s, abs_T) in
    1.96 -      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
    1.97 -      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
    1.98 -    end
    1.99 -
   1.100 -fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
   1.101 -  | loose_bvar1_count (t1 $ t2, k) =
   1.102 -    loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
   1.103 -  | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
   1.104 -  | loose_bvar1_count _ = 0
   1.105 -
   1.106 -fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
   1.107 -  | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
   1.108 -  | s_betapply Ts (Const (@{const_name Let},
   1.109 -                          Type (_, [bound_T, Type (_, [_, body_T])]))
   1.110 -                   $ t12 $ Abs (s, T, t13'), t2) =
   1.111 -    let val body_T' = range_type body_T in
   1.112 -      Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T')
   1.113 -      $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
   1.114 -    end
   1.115 -  | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
   1.116 -    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
   1.117 -              (curry betapply t1) t2
   1.118 -     handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
   1.119 -  | s_betapply _ (t1, t2) = t1 $ t2
   1.120 -fun s_betapplys Ts = Library.foldl (s_betapply Ts)
   1.121 -
   1.122 -fun s_beta_norm Ts t =
   1.123 -  let
   1.124 -    fun aux _ (Var _) = raise Same.SAME
   1.125 -      | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
   1.126 -      | aux Ts ((t1 as Abs _) $ t2) =
   1.127 -        Same.commit (aux Ts) (s_betapply Ts (t1, t2))
   1.128 -      | aux Ts (t1 $ t2) =
   1.129 -        ((case aux Ts t1 of
   1.130 -           t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
   1.131 -         | t1 => t1 $ Same.commit (aux Ts) t2)
   1.132 -        handle Same.SAME => t1 $ aux Ts t2)
   1.133 -      | aux _ _ = raise Same.SAME
   1.134 -  in aux Ts t handle Same.SAME => t end
   1.135 -
   1.136  fun s_conj (t1, @{const True}) = t1
   1.137    | s_conj (@{const True}, t2) = t2
   1.138    | s_conj (t1, t2) =
   1.139 @@ -568,6 +493,9 @@
   1.140        |> these |> null |> not
   1.141    | is_frac_type _ _ = false
   1.142  fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
   1.143 +fun is_higher_order_type (Type (@{type_name fun}, _)) = true
   1.144 +  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   1.145 +  | is_higher_order_type _ = false
   1.146  
   1.147  fun iterator_type_for_const gfp (s, T) =
   1.148    Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
   1.149 @@ -1014,6 +942,162 @@
   1.150      |> the |> pair s
   1.151    end
   1.152  
   1.153 +fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
   1.154 +    reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
   1.155 +  | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
   1.156 +    card_of_type assigns T1 * card_of_type assigns T2
   1.157 +  | card_of_type _ (Type (@{type_name itself}, _)) = 1
   1.158 +  | card_of_type _ @{typ prop} = 2
   1.159 +  | card_of_type _ @{typ bool} = 2
   1.160 +  | card_of_type assigns T =
   1.161 +    case AList.lookup (op =) assigns T of
   1.162 +      SOME k => k
   1.163 +    | NONE => if T = @{typ bisim_iterator} then 0
   1.164 +              else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
   1.165 +
   1.166 +fun bounded_card_of_type max default_card assigns
   1.167 +                         (Type (@{type_name fun}, [T1, T2])) =
   1.168 +    let
   1.169 +      val k1 = bounded_card_of_type max default_card assigns T1
   1.170 +      val k2 = bounded_card_of_type max default_card assigns T2
   1.171 +    in
   1.172 +      if k1 = max orelse k2 = max then max
   1.173 +      else Int.min (max, reasonable_power k2 k1)
   1.174 +    end
   1.175 +  | bounded_card_of_type max default_card assigns
   1.176 +                         (Type (@{type_name prod}, [T1, T2])) =
   1.177 +    let
   1.178 +      val k1 = bounded_card_of_type max default_card assigns T1
   1.179 +      val k2 = bounded_card_of_type max default_card assigns T2
   1.180 +    in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
   1.181 +  | bounded_card_of_type max default_card assigns T =
   1.182 +    Int.min (max, if default_card = ~1 then
   1.183 +                    card_of_type assigns T
   1.184 +                  else
   1.185 +                    card_of_type assigns T
   1.186 +                    handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   1.187 +                           default_card)
   1.188 +
   1.189 +fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
   1.190 +                               assigns T =
   1.191 +  let
   1.192 +    fun aux avoid T =
   1.193 +      (if member (op =) avoid T then
   1.194 +         0
   1.195 +       else if member (op =) finitizable_dataTs T then
   1.196 +         raise SAME ()
   1.197 +       else case T of
   1.198 +         Type (@{type_name fun}, [T1, T2]) =>
   1.199 +         let
   1.200 +           val k1 = aux avoid T1
   1.201 +           val k2 = aux avoid T2
   1.202 +         in
   1.203 +           if k1 = 0 orelse k2 = 0 then 0
   1.204 +           else if k1 >= max orelse k2 >= max then max
   1.205 +           else Int.min (max, reasonable_power k2 k1)
   1.206 +         end
   1.207 +       | Type (@{type_name prod}, [T1, T2]) =>
   1.208 +         let
   1.209 +           val k1 = aux avoid T1
   1.210 +           val k2 = aux avoid T2
   1.211 +         in
   1.212 +           if k1 = 0 orelse k2 = 0 then 0
   1.213 +           else if k1 >= max orelse k2 >= max then max
   1.214 +           else Int.min (max, k1 * k2)
   1.215 +         end
   1.216 +       | Type (@{type_name itself}, _) => 1
   1.217 +       | @{typ prop} => 2
   1.218 +       | @{typ bool} => 2
   1.219 +       | Type _ =>
   1.220 +         (case datatype_constrs hol_ctxt T of
   1.221 +            [] => if is_integer_type T orelse is_bit_type T then 0
   1.222 +                  else raise SAME ()
   1.223 +          | constrs =>
   1.224 +            let
   1.225 +              val constr_cards =
   1.226 +                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
   1.227 +                    constrs
   1.228 +            in
   1.229 +              if exists (curry (op =) 0) constr_cards then 0
   1.230 +              else Integer.sum constr_cards
   1.231 +            end)
   1.232 +       | _ => raise SAME ())
   1.233 +      handle SAME () =>
   1.234 +             AList.lookup (op =) assigns T |> the_default default_card
   1.235 +  in Int.min (max, aux [] T) end
   1.236 +
   1.237 +val typical_atomic_card = 4
   1.238 +val typical_card_of_type = bounded_card_of_type 65536 typical_atomic_card []
   1.239 +
   1.240 +val small_type_max_card = 5
   1.241 +
   1.242 +fun is_finite_type hol_ctxt T =
   1.243 +  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
   1.244 +fun is_small_finite_type hol_ctxt T =
   1.245 +  let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
   1.246 +    n > 0 andalso n <= small_type_max_card
   1.247 +  end
   1.248 +
   1.249 +fun is_special_eligible_arg strict Ts t =
   1.250 +  case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
   1.251 +    [] => true
   1.252 +  | bad_Ts =>
   1.253 +    let
   1.254 +      val bad_Ts_cost = fold (Integer.max o typical_card_of_type) bad_Ts 0
   1.255 +      val T_cost = typical_card_of_type (fastype_of1 (Ts, t))
   1.256 +    in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end
   1.257 +
   1.258 +fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
   1.259 +
   1.260 +fun let_var s = (nitpick_prefix ^ s, 999)
   1.261 +val let_inline_threshold = 20
   1.262 +
   1.263 +fun s_let Ts s n abs_T body_T f t =
   1.264 +  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
   1.265 +     is_special_eligible_arg false Ts t then
   1.266 +    f t
   1.267 +  else
   1.268 +    let val z = (let_var s, abs_T) in
   1.269 +      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
   1.270 +      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
   1.271 +    end
   1.272 +
   1.273 +fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
   1.274 +  | loose_bvar1_count (t1 $ t2, k) =
   1.275 +    loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
   1.276 +  | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
   1.277 +  | loose_bvar1_count _ = 0
   1.278 +
   1.279 +fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
   1.280 +  | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
   1.281 +  | s_betapply Ts (Const (@{const_name Let},
   1.282 +                          Type (_, [bound_T, Type (_, [_, body_T])]))
   1.283 +                   $ t12 $ Abs (s, T, t13'), t2) =
   1.284 +    let val body_T' = range_type body_T in
   1.285 +      Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T')
   1.286 +      $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
   1.287 +    end
   1.288 +  | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
   1.289 +    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
   1.290 +              (curry betapply t1) t2
   1.291 +     handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
   1.292 +  | s_betapply _ (t1, t2) = t1 $ t2
   1.293 +fun s_betapplys Ts = Library.foldl (s_betapply Ts)
   1.294 +
   1.295 +fun s_beta_norm Ts t =
   1.296 +  let
   1.297 +    fun aux _ (Var _) = raise Same.SAME
   1.298 +      | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
   1.299 +      | aux Ts ((t1 as Abs _) $ t2) =
   1.300 +        Same.commit (aux Ts) (s_betapply Ts (t1, t2))
   1.301 +      | aux Ts (t1 $ t2) =
   1.302 +        ((case aux Ts t1 of
   1.303 +           t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
   1.304 +         | t1 => t1 $ Same.commit (aux Ts) t2)
   1.305 +        handle Same.SAME => t1 $ aux Ts t2)
   1.306 +      | aux _ _ = raise Same.SAME
   1.307 +  in aux Ts t handle Same.SAME => t end
   1.308 +
   1.309  fun discr_term_for_constr hol_ctxt (x as (s, T)) =
   1.310    let val dataT = body_type T in
   1.311      if s = @{const_name Suc} then
   1.312 @@ -1150,97 +1234,6 @@
   1.313          raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
   1.314      | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
   1.315  
   1.316 -fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
   1.317 -    reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
   1.318 -  | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
   1.319 -    card_of_type assigns T1 * card_of_type assigns T2
   1.320 -  | card_of_type _ (Type (@{type_name itself}, _)) = 1
   1.321 -  | card_of_type _ @{typ prop} = 2
   1.322 -  | card_of_type _ @{typ bool} = 2
   1.323 -  | card_of_type assigns T =
   1.324 -    case AList.lookup (op =) assigns T of
   1.325 -      SOME k => k
   1.326 -    | NONE => if T = @{typ bisim_iterator} then 0
   1.327 -              else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
   1.328 -fun bounded_card_of_type max default_card assigns
   1.329 -                         (Type (@{type_name fun}, [T1, T2])) =
   1.330 -    let
   1.331 -      val k1 = bounded_card_of_type max default_card assigns T1
   1.332 -      val k2 = bounded_card_of_type max default_card assigns T2
   1.333 -    in
   1.334 -      if k1 = max orelse k2 = max then max
   1.335 -      else Int.min (max, reasonable_power k2 k1)
   1.336 -    end
   1.337 -  | bounded_card_of_type max default_card assigns
   1.338 -                         (Type (@{type_name prod}, [T1, T2])) =
   1.339 -    let
   1.340 -      val k1 = bounded_card_of_type max default_card assigns T1
   1.341 -      val k2 = bounded_card_of_type max default_card assigns T2
   1.342 -    in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
   1.343 -  | bounded_card_of_type max default_card assigns T =
   1.344 -    Int.min (max, if default_card = ~1 then
   1.345 -                    card_of_type assigns T
   1.346 -                  else
   1.347 -                    card_of_type assigns T
   1.348 -                    handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   1.349 -                           default_card)
   1.350 -fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
   1.351 -                               assigns T =
   1.352 -  let
   1.353 -    fun aux avoid T =
   1.354 -      (if member (op =) avoid T then
   1.355 -         0
   1.356 -       else if member (op =) finitizable_dataTs T then
   1.357 -         raise SAME ()
   1.358 -       else case T of
   1.359 -         Type (@{type_name fun}, [T1, T2]) =>
   1.360 -         let
   1.361 -           val k1 = aux avoid T1
   1.362 -           val k2 = aux avoid T2
   1.363 -         in
   1.364 -           if k1 = 0 orelse k2 = 0 then 0
   1.365 -           else if k1 >= max orelse k2 >= max then max
   1.366 -           else Int.min (max, reasonable_power k2 k1)
   1.367 -         end
   1.368 -       | Type (@{type_name prod}, [T1, T2]) =>
   1.369 -         let
   1.370 -           val k1 = aux avoid T1
   1.371 -           val k2 = aux avoid T2
   1.372 -         in
   1.373 -           if k1 = 0 orelse k2 = 0 then 0
   1.374 -           else if k1 >= max orelse k2 >= max then max
   1.375 -           else Int.min (max, k1 * k2)
   1.376 -         end
   1.377 -       | Type (@{type_name itself}, _) => 1
   1.378 -       | @{typ prop} => 2
   1.379 -       | @{typ bool} => 2
   1.380 -       | Type _ =>
   1.381 -         (case datatype_constrs hol_ctxt T of
   1.382 -            [] => if is_integer_type T orelse is_bit_type T then 0
   1.383 -                  else raise SAME ()
   1.384 -          | constrs =>
   1.385 -            let
   1.386 -              val constr_cards =
   1.387 -                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
   1.388 -                    constrs
   1.389 -            in
   1.390 -              if exists (curry (op =) 0) constr_cards then 0
   1.391 -              else Integer.sum constr_cards
   1.392 -            end)
   1.393 -       | _ => raise SAME ())
   1.394 -      handle SAME () =>
   1.395 -             AList.lookup (op =) assigns T |> the_default default_card
   1.396 -  in Int.min (max, aux [] T) end
   1.397 -
   1.398 -val small_type_max_card = 5
   1.399 -
   1.400 -fun is_finite_type hol_ctxt T =
   1.401 -  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
   1.402 -fun is_small_finite_type hol_ctxt T =
   1.403 -  let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
   1.404 -    n > 0 andalso n <= small_type_max_card
   1.405 -  end
   1.406 -
   1.407  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
   1.408    | is_ground_term (Const _) = true
   1.409    | is_ground_term _ = false
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 28 17:53:10 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 28 17:53:10 2011 +0100
     2.3 @@ -1165,12 +1165,10 @@
     2.4                   aux "" [] [] t1 $ aux "" [] [] t2
     2.5                 else
     2.6                   let
     2.7 -                   val typical_card = 4
     2.8                     fun big_union proj ps =
     2.9                       fold (fold (insert (op =)) o proj) ps []
    2.10                     val (ts, connective) = strip_any_connective t
    2.11 -                   val T_costs =
    2.12 -                     map (bounded_card_of_type 65536 typical_card []) Ts
    2.13 +                   val T_costs = map typical_card_of_type Ts
    2.14                     val t_costs = map size_of_term ts
    2.15                     val num_Ts = length Ts
    2.16                     val flip = curry (op -) (num_Ts - 1)