--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sun Aug 01 18:57:49 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sun Aug 01 23:15:26 2010 +0200
@@ -259,8 +259,10 @@
fun axiom_for_built_in_rel (x as (n, j)) =
if n = 2 andalso j <= suc_rels_base then
let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
- if tabulate orelse k < 2 then
+ if tabulate then
NONE
+ else if k < 2 then
+ SOME (KK.No (KK.Rel x))
else
SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1)))
end