merged
authorpopescua
Tue, 28 May 2013 18:51:29 +0200
changeset 52204 a3bad3bb9276
parent 52203 055c392e79cf (current diff)
parent 52202 d5c80b12a1f2 (diff)
child 52206 6fa21e5a57c3
merged
--- 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,
--- 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
     ()