--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 25 09:16:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 25 10:08:44 2010 +0100
@@ -1096,8 +1096,8 @@
in Int.min (max, aux [] T) end
(* hol_context -> typ -> bool *)
-fun is_finite_type hol_ctxt =
- not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
+fun is_finite_type hol_ctxt T =
+ bounded_exact_card_of_type hol_ctxt 1 2 [] T <> 0
(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2