src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 35384 88dbcfe75c45
parent 35335 f715cfde056a
child 35385 29f81babefd7
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 09:16:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 10:08:44 2010 +0100
     1.3 @@ -1096,8 +1096,8 @@
     1.4    in Int.min (max, aux [] T) end
     1.5  
     1.6  (* hol_context -> typ -> bool *)
     1.7 -fun is_finite_type hol_ctxt =
     1.8 -  not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
     1.9 +fun is_finite_type hol_ctxt T =
    1.10 +  bounded_exact_card_of_type hol_ctxt 1 2 [] T <> 0
    1.11  
    1.12  (* term -> bool *)
    1.13  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2