# HG changeset patch
# User blanchet
# Date 1299662729 -3600
# Node ID c24e7fd1746445eb1b8f8f8ebadee29c0f55216c
# Parent  582cccdda0ed4c4494dab3754cc8034efbce3d3b
perform no arity check in debug mode so that we get to see the Kodkod problem

diff -r 582cccdda0ed -r c24e7fd17464 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Mar 04 17:39:30 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 09 10:25:29 2011 +0100
@@ -521,7 +521,8 @@
         val min_univ_card =
           NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table
                          (univ_card nat_card int_card main_j0 [] KK.True)
-        val _ = check_arity guiltiest_party min_univ_card min_highest_arity
+        val _ = if debug then ()
+                else check_arity guiltiest_party min_univ_card min_highest_arity
 
         val def_us =
           def_us |> map (choose_reps_in_nut scope unsound rep_table true)
@@ -584,7 +585,7 @@
           fold Integer.max (map (fst o fst) (maps fst bounds)) 0
         val formula = fold_rev s_and axioms formula
         val _ = if bits = 0 then () else check_bits bits formula
-        val _ = if formula = KK.False then ()
+        val _ = if debug orelse formula = KK.False then ()
                 else check_arity "" univ_card highest_arity
       in
         SOME ({comment = comment, settings = settings, univ_card = univ_card,