# HG changeset patch # User popescua # Date 1369759889 -7200 # Node ID a3bad3bb9276390a16a2abcc0ba3cd50f658042c # Parent 055c392e79cf830ea50548a9c553a42c321d2b79# Parent d5c80b12a1f2ddab2437fc8fa3e85be1b76b98e0 merged diff -r 055c392e79cf -r a3bad3bb9276 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue May 28 16:56:49 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue May 28 18:51:29 2013 +0200 @@ -544,8 +544,7 @@ 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 _ = if debug then () - else check_arity guiltiest_party min_univ_card min_highest_arity + val _ = 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) @@ -612,7 +611,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 debug orelse formula = KK.False then () + val _ = if formula = KK.False then () else check_arity "" univ_card highest_arity in SOME ({comment = comment, settings = settings, univ_card = univ_card, diff -r 055c392e79cf -r a3bad3bb9276 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue May 28 16:56:49 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue May 28 18:51:29 2013 +0200 @@ -104,7 +104,7 @@ else " of Kodkod relation associated with " ^ quote (original_name guilty_party)) ^ - " too large for universe of cardinality " ^ + " too large for a universe of size " ^ string_of_int univ_card) else ()