src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 41860 49d0fc8c418c
parent 41803 ef13e3b7cbaf
child 41870 a14a492f472f
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 28 17:53:10 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 28 17:53:10 2011 +0100
@@ -1165,12 +1165,10 @@
                  aux "" [] [] t1 $ aux "" [] [] t2
                else
                  let
-                   val typical_card = 4
                    fun big_union proj ps =
                      fold (fold (insert (op =)) o proj) ps []
                    val (ts, connective) = strip_any_connective t
-                   val T_costs =
-                     map (bounded_card_of_type 65536 typical_card []) Ts
+                   val T_costs = map typical_card_of_type Ts
                    val t_costs = map size_of_term ts
                    val num_Ts = length Ts
                    val flip = curry (op -) (num_Ts - 1)