Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 45402 1fac64bbdb4f
parent 45399 fdc73782278f
child 46083 efeaa79f021b 
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Nov 08 08:56:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Nov 08 08:56:24 2011 +0100
@@ -447,7 +447,7 @@
     fun is_concrete facto =
       is_word_type T orelse
       (* FIXME: looks wrong other types than just functions might be
-         abstract. *)
+         abstract. "is_complete" is also suspicious. *)
       xs |> maps (binder_types o snd) |> maps binder_types
          |> forall (has_exact_card hol_ctxt facto finitizable_dataTs
                                    card_assigns)
isabelle