author | blanchet |
Mon, 07 Nov 2011 22:59:24 +0100 | |
changeset 45399 | fdc73782278f |
parent 45398 | 7dbb7b044a11 |
child 45400 | e4e9394ddb0c |
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Nov 07 22:22:01 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Nov 07 22:59:24 2011 +0100 @@ -446,6 +446,8 @@ has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T fun is_concrete facto = is_word_type T orelse + (* FIXME: looks wrong other types than just functions might be + abstract. *) xs |> maps (binder_types o snd) |> maps binder_types |> forall (has_exact_card hol_ctxt facto finitizable_dataTs card_assigns)