src/HOL/Tools/Nitpick/nitpick_scope.ML
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)