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_kodkod.ML
changeset 33631 d3af5b21cbaf
parent 33582 bdf98e327f0b
child 33705 947184dc75c9 
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Nov 12 09:11:46 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Nov 12 14:47:54 2009 +0100
@@ -1448,7 +1448,7 @@
           fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel
       | Op2 (Apply, _, R, u1, u2) =>
         if is_Cst Unrep u2 andalso is_set_type (type_of u1)
-           andalso not (is_opt_rep (rep_of u1)) then
+           andalso is_FreeName u1 then
           false_atom
         else
           to_apply R u1 u2
isabelle