# HG changeset patch
# User blanchet
# Date 1280697326 -7200
# Node ID d04aceff43cf3e81386ca7ccbd22e1a0bf72548a
# Parent  faa18bf13b9b4274654430d02f2f38b1b83ea575
fix minor bug in sym breaking

diff -r faa18bf13b9b -r d04aceff43cf src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- 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