Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweaked comment
authorblanchet
Tue, 08 Nov 2011 08:56:24 +0100
changeset 45402 1fac64bbdb4f
parent 45401 36478a5f6104
child 45403 7a0b8debef77
child 45408 7156f63ce3c2
tweaked comment
src/HOL/Tools/Nitpick/nitpick_scope.ML file | annotate | diff | comparison | revisions 
--- 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