added FIXME comment
authorblanchet
Mon, 07 Nov 2011 22:59:24 +0100
changeset 46267fdc73782278f
parent 46266 7dbb7b044a11
child 46271 e4e9394ddb0c
added FIXME comment
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Nov 07 22:22:01 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Nov 07 22:59:24 2011 +0100
     1.3 @@ -446,6 +446,8 @@
     1.4        has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
     1.5      fun is_concrete facto =
     1.6        is_word_type T orelse
     1.7 +      (* FIXME: looks wrong other types than just functions might be
     1.8 +         abstract. *)
     1.9        xs |> maps (binder_types o snd) |> maps binder_types
    1.10           |> forall (has_exact_card hol_ctxt facto finitizable_dataTs
    1.11                                     card_assigns)