changeset 45399 | fdc73782278f |
parent 41991 | ea02b9ee3085 |
child 45402 | 1fac64bbdb4f |
--- 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)