# HG changeset patch
# User blanchet
# Date 1280841317 -7200
# Node ID 747f8077b09ace1020826a451f2607db9b02267a
# Parent  6f9f80afaf4f2a95dbea2c74414c6b018d6c37a8
more helpful message

diff -r 6f9f80afaf4f -r 747f8077b09a src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 03 14:54:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 03 15:15:17 2010 +0200
@@ -466,12 +466,15 @@
         val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
         val (nonsel_names, rep_table) =
           choose_reps_for_consts scope all_exact nonsel_names rep_table
-        val min_highest_arity =
-          NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1
+        val (guiltiest_party, min_highest_arity) =
+          NameTable.fold (fn (name, R) => fn (s, n) =>
+                             let val n' = arity_of_rep R in
+                               if n' > n then (nickname_of name, n') else (s, n)
+                             end) rep_table ("", 1)
         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 min_univ_card min_highest_arity
+        val _ = check_arity guiltiest_party min_univ_card min_highest_arity
 
         val def_us = map (choose_reps_in_nut scope unsound rep_table true)
                          def_us
@@ -533,7 +536,7 @@
         val formula = fold_rev s_and axioms formula
         val _ = if bits = 0 then () else check_bits bits formula
         val _ = if formula = KK.False then ()
-                else check_arity univ_card highest_arity
+                else check_arity "" univ_card highest_arity
       in
         SOME ({comment = comment, settings = settings, univ_card = univ_card,
                tuple_assigns = [], bounds = bounds,
diff -r 6f9f80afaf4f -r 747f8077b09a src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Aug 03 14:54:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Aug 03 15:15:17 2010 +0200
@@ -17,7 +17,7 @@
   val univ_card :
     int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
   val check_bits : int -> Kodkod.formula -> unit
-  val check_arity : int -> int -> unit
+  val check_arity : string -> int -> int -> unit
   val kk_tuple : bool -> int -> int list -> Kodkod.tuple
   val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
   val sequential_int_bounds : int -> Kodkod.int_bound list
@@ -93,11 +93,17 @@
                   int_expr_func = int_expr_func}
   in KK.fold_formula expr_F formula () end
 
-fun check_arity univ_card n =
+fun check_arity guilty_party univ_card n =
   if n > KK.max_arity univ_card then
     raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
-                     "arity " ^ string_of_int n ^ " too large for universe of \
-                     \cardinality " ^ string_of_int univ_card)
+                     "arity " ^ string_of_int n ^
+                     (if guilty_party = "" then
+                        ""
+                      else
+                        " of Kodkod relation associated with " ^
+                        quote guilty_party) ^
+                     " too large for universe of cardinality " ^
+                     string_of_int univ_card)
   else
     ()
 
@@ -200,7 +206,7 @@
 
 fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0
                           (x as (n, _)) =
-  (check_arity univ_card n;
+  (check_arity "" univ_card n;
    if x = not3_rel then
      ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
    else if x = suc_rel then